---

Step * of Lemma antecedent-surjection_functionality_wrt_iff

∀es:EO
  ∀[P1,P2,Q1,Q2:E ⟶ ℙ].
    ∀f:{e:E| P1 e}  ⟶ {e:E| Q1 e} 
      ((∀e:E. (P1 e ⇐⇒ P2 e)) ⇒ (∀e:E. (Q1 e ⇐⇒ Q2 e)) ⇒ (Q1 ←⟵ f── P1 ⇐⇒ Q2 ←⟵ f── P2))
BY
{ (Auto
   THEN Try (Complete (Auto))
   THEN Try ((RepeatFor 3 (ParallelLast)
              THEN Try (RepeatFor 3 (ParallelLast))
              THEN skip{(Auto THEN ParallelLast THEN Auto)}))) }

1
1. es : EO@i'
2. [P1] : E ⟶ ℙ
3. [P2] : E ⟶ ℙ
4. [Q1] : E ⟶ ℙ
5. [Q2] : E ⟶ ℙ
6. f : {e:E| P1 e}  ⟶ {e:E| Q1 e} @i
7. ∀e:E. (P1 e ⇐⇒ P2 e)@i
8. ∀e:E. (Q1 e ⇐⇒ Q2 e)@i
9. ∀e:{e:E| Q1 e} . ∃e':{e:E| P1 e} . ((f e') = e ∈ E)@i
10. ∀e:{e:E| P1 e} . ((f e < e) ∧ (Q1 (f e)))@i
⊢ ∀e:{e:E| P2 e} . ((f e < e) ∧ (Q2 (f e)))

2
1. es : EO@i'
2. [P1] : E ⟶ ℙ
3. [P2] : E ⟶ ℙ
4. [Q1] : E ⟶ ℙ
5. [Q2] : E ⟶ ℙ
6. f : {e:E| P1 e}  ⟶ {e:E| Q1 e} @i
7. ∀e:E. (P1 e ⇐⇒ P2 e)@i
8. ∀e:E. (Q1 e ⇐⇒ Q2 e)@i
9. ∀e:{e:E| Q2 e} . ∃e':{e:E| P2 e} . ((f e') = e ∈ E)@i
10. ∀e:{e:E| P2 e} . ((f e < e) ∧ (Q2 (f e)))@i
⊢ ∀e:{e:E| P1 e} . ((f e < e) ∧ (Q1 (f e)))

---

Latex:

---

Latex:
\mforall{}es:EO
    \mforall{}[P1,P2,Q1,Q2:E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f:\{e:E|  P1  e\}    {}\mrightarrow{}  \{e:E|  Q1  e\} 
            ((\mforall{}e:E.  (P1  e  \mLeftarrow{}{}\mRightarrow{}  P2  e))  {}\mRightarrow{}  (\mforall{}e:E.  (Q1  e  \mLeftarrow{}{}\mRightarrow{}  Q2  e))  {}\mRightarrow{}  (Q1  \mleftarrow{}\mleftarrow{}{}  f{}{}  P1  \mLeftarrow{}{}\mRightarrow{}  Q2  \mleftarrow{}\mleftarrow{}{}  f{}{}  P2))


By

---

Latex:
(Auto
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((RepeatFor  3  (ParallelLast)
                        THEN  Try  (RepeatFor  3  (ParallelLast))
                        THEN  skip\{(Auto  THEN  ParallelLast  THEN  Auto)\})))

---

Home Index