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 ⇐⇒ P2 e))  (∀e:E. (Q1 ⇐⇒ Q2 e))  (Q1 ←←─ f── P1 ⇐⇒ Q2 ←←─ f── P2))
BY
(Auto
   THEN Try (Complete (Auto))
   THEN Try ((RepeatFor (ParallelLast)
              THEN Try (RepeatFor (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. {e:E| P1 e}  ─→ {e:E| Q1 e} @i
7. ∀e:E. (P1 ⇐⇒ P2 e)@i
8. ∀e:E. (Q1 ⇐⇒ 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. {e:E| P1 e}  ─→ {e:E| Q1 e} @i
7. ∀e:E. (P1 ⇐⇒ P2 e)@i
8. ∀e:E. (Q1 ⇐⇒ 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:


\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

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




Home Index