This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
wemaplem2.p ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐵 ↑m 𝐴 ) )
wemaplem2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m 𝐴 ) )
wemaplem2.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝐵 ↑m 𝐴 ) )
wemaplem2.r ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
wemaplem2.s ⊢ ( 𝜑 → 𝑆 Po 𝐵 )
wemaplem3.px ⊢ ( 𝜑 → 𝑃 𝑇 𝑋 )
wemaplem3.xq ⊢ ( 𝜑 → 𝑋 𝑇 𝑄 )
Assertion wemaplem3 ( 𝜑 → 𝑃 𝑇 𝑄 )

Proof

Step Hyp Ref Expression
1 wemapso.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
2 wemaplem2.p ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐵 ↑m 𝐴 ) )
3 wemaplem2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m 𝐴 ) )
4 wemaplem2.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝐵 ↑m 𝐴 ) )
5 wemaplem2.r ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
6 wemaplem2.s ⊢ ( 𝜑 → 𝑆 Po 𝐵 )
7 wemaplem3.px ⊢ ( 𝜑 → 𝑃 𝑇 𝑋 )
8 wemaplem3.xq ⊢ ( 𝜑 → 𝑋 𝑇 𝑄 )
9 1 wemaplem1 ⊢ ( ( 𝑃 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐴 ) ) → ( 𝑃 𝑇 𝑋 ↔ ∃ 𝑎 ∈ 𝐴 ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) )
10 2 3 9 syl2anc ⊢ ( 𝜑 → ( 𝑃 𝑇 𝑋 ↔ ∃ 𝑎 ∈ 𝐴 ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) )
11 7 10 mpbid ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐴 ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) )
12 1 wemaplem1 ⊢ ( ( 𝑋 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑄 ∈ ( 𝐵 ↑m 𝐴 ) ) → ( 𝑋 𝑇 𝑄 ↔ ∃ 𝑏 ∈ 𝐴 ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) )
13 3 4 12 syl2anc ⊢ ( 𝜑 → ( 𝑋 𝑇 𝑄 ↔ ∃ 𝑏 ∈ 𝐴 ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) )
14 8 13 mpbid ⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐴 ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
15 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → 𝑃 ∈ ( 𝐵 ↑m 𝐴 ) )
16 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → 𝑋 ∈ ( 𝐵 ↑m 𝐴 ) )
17 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → 𝑄 ∈ ( 𝐵 ↑m 𝐴 ) )
18 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → 𝑅 Or 𝐴 )
19 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → 𝑆 Po 𝐵 )
20 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → 𝑎 ∈ 𝐴 )
21 simp2rl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) )
22 21 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) )
23 simprr ⊢ ( ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) )
24 23 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) )
25 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → 𝑏 ∈ 𝐴 )
26 simprrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) )
27 simprrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) )
28 1 15 16 17 18 19 20 22 24 25 26 27 wemaplem2 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) → 𝑃 𝑇 𝑄 )
29 28 rexlimdvaa ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) ) ) → ( ∃ 𝑏 ∈ 𝐴 ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → 𝑃 𝑇 𝑄 ) )
30 29 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) → ( ∃ 𝑏 ∈ 𝐴 ( ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → 𝑃 𝑇 𝑄 ) ) )
31 11 14 30 mp2d ⊢ ( 𝜑 → 𝑃 𝑇 𝑄 )