Metamath Proof Explorer

Theorem wemaplem3

Description: Lemma for wemapso . Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015) (Revised by AV, 21-Jul-2024)

Ref Expression
Hypotheses wemapso.t ⊢ T = x y | ∃ z ∈ A x ⁡ z S y ⁡ z ∧ ∀ w ∈ A w R z → x ⁡ w = y ⁡ w
wemaplem2.p ⊢ φ → P ∈ B A
wemaplem2.x ⊢ φ → X ∈ B A
wemaplem2.q ⊢ φ → Q ∈ B A
wemaplem2.r ⊢ φ → R Or A
wemaplem2.s ⊢ φ → S Po B
wemaplem3.px ⊢ φ → P T X
wemaplem3.xq ⊢ φ → X T Q
Assertion wemaplem3 ⊢ φ → P T Q

Proof

Step Hyp Ref Expression
1 wemapso.t ⊢ T = x y | ∃ z ∈ A x ⁡ z S y ⁡ z ∧ ∀ w ∈ A w R z → x ⁡ w = y ⁡ w
2 wemaplem2.p ⊢ φ → P ∈ B A
3 wemaplem2.x ⊢ φ → X ∈ B A
4 wemaplem2.q ⊢ φ → Q ∈ B A
5 wemaplem2.r ⊢ φ → R Or A
6 wemaplem2.s ⊢ φ → S Po B
7 wemaplem3.px ⊢ φ → P T X
8 wemaplem3.xq ⊢ φ → X T Q
9 1 wemaplem1 ⊢ P ∈ B A ∧ X ∈ B A → P T X ↔ ∃ a ∈ A P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c
10 2 3 9 syl2anc ⊢ φ → P T X ↔ ∃ a ∈ A P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c
11 7 10 mpbid ⊢ φ → ∃ a ∈ A P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c
12 1 wemaplem1 ⊢ X ∈ B A ∧ Q ∈ B A → X T Q ↔ ∃ b ∈ A X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c
13 3 4 12 syl2anc ⊢ φ → X T Q ↔ ∃ b ∈ A X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c
14 8 13 mpbid ⊢ φ → ∃ b ∈ A X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c
15 2 ad2antrr ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → P ∈ B A
16 3 ad2antrr ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → X ∈ B A
17 4 ad2antrr ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → Q ∈ B A
18 5 ad2antrr ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → R Or A
19 6 ad2antrr ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → S Po B
20 simplrl ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → a ∈ A
21 simp2rl ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → P ⁡ a S X ⁡ a
22 21 3expa ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → P ⁡ a S X ⁡ a
23 simprr ⊢ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c → ∀ c ∈ A c R a → P ⁡ c = X ⁡ c
24 23 ad2antlr ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → ∀ c ∈ A c R a → P ⁡ c = X ⁡ c
25 simprl ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → b ∈ A
26 simprrl ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → X ⁡ b S Q ⁡ b
27 simprrr ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c
28 1 15 16 17 18 19 20 22 24 25 26 27 wemaplem2 ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c ∧ b ∈ A ∧ X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → P T Q
29 28 rexlimdvaa ⊢ φ ∧ a ∈ A ∧ P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c → ∃ b ∈ A X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → P T Q
30 29 rexlimdvaa ⊢ φ → ∃ a ∈ A P ⁡ a S X ⁡ a ∧ ∀ c ∈ A c R a → P ⁡ c = X ⁡ c → ∃ b ∈ A X ⁡ b S Q ⁡ b ∧ ∀ c ∈ A c R b → X ⁡ c = Q ⁡ c → P T Q
31 11 14 30 mp2d ⊢ φ → P T Q