Metamath Proof Explorer

Theorem wemaplem2

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 𝐵 )
wemaplem2.px1 ⊢ ( 𝜑 → 𝑎 ∈ 𝐴 )
wemaplem2.px2 ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) )
wemaplem2.px3 ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) )
wemaplem2.xq1 ⊢ ( 𝜑 → 𝑏 ∈ 𝐴 )
wemaplem2.xq2 ⊢ ( 𝜑 → ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) )
wemaplem2.xq3 ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) )
Assertion wemaplem2 ( 𝜑 → 𝑃 𝑇 𝑄 )

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 wemaplem2.px1 ⊢ ( 𝜑 → 𝑎 ∈ 𝐴 )
8 wemaplem2.px2 ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) )
9 wemaplem2.px3 ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) )
10 wemaplem2.xq1 ⊢ ( 𝜑 → 𝑏 ∈ 𝐴 )
11 wemaplem2.xq2 ⊢ ( 𝜑 → ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) )
12 wemaplem2.xq3 ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) )
13 7 10 ifcld ⊢ ( 𝜑 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ∈ 𝐴 )
14 8 adantr ⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) )
15 breq1 ⊢ ( 𝑐 = 𝑎 → ( 𝑐 𝑅 𝑏 ↔ 𝑎 𝑅 𝑏 ) )
16 fveq2 ⊢ ( 𝑐 = 𝑎 → ( 𝑋 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑎 ) )
17 fveq2 ⊢ ( 𝑐 = 𝑎 → ( 𝑄 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑎 ) )
18 16 17 eqeq12d ⊢ ( 𝑐 = 𝑎 → ( ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ↔ ( 𝑋 ‘ 𝑎 ) = ( 𝑄 ‘ 𝑎 ) ) )
19 15 18 imbi12d ⊢ ( 𝑐 = 𝑎 → ( ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ↔ ( 𝑎 𝑅 𝑏 → ( 𝑋 ‘ 𝑎 ) = ( 𝑄 ‘ 𝑎 ) ) ) )
20 19 12 7 rspcdva ⊢ ( 𝜑 → ( 𝑎 𝑅 𝑏 → ( 𝑋 ‘ 𝑎 ) = ( 𝑄 ‘ 𝑎 ) ) )
21 20 imp ⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( 𝑋 ‘ 𝑎 ) = ( 𝑄 ‘ 𝑎 ) )
22 14 21 breqtrd ⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) )
23 iftrue ⊢ ( 𝑎 𝑅 𝑏 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) = 𝑎 )
24 23 fveq2d ⊢ ( 𝑎 𝑅 𝑏 → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑃 ‘ 𝑎 ) )
25 23 fveq2d ⊢ ( 𝑎 𝑅 𝑏 → ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑄 ‘ 𝑎 ) )
26 24 25 breq12d ⊢ ( 𝑎 𝑅 𝑏 → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ) )
28 22 27 mpbird ⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) )
29 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → 𝑆 Po 𝐵 )
30 elmapi ⊢ ( 𝑃 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑃 : 𝐴 ⟶ 𝐵 )
31 2 30 syl ⊢ ( 𝜑 → 𝑃 : 𝐴 ⟶ 𝐵 )
32 31 10 ffvelcdmd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 )
33 elmapi ⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑋 : 𝐴 ⟶ 𝐵 )
34 3 33 syl ⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ 𝐵 )
35 34 10 ffvelcdmd ⊢ ( 𝜑 → ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 )
36 elmapi ⊢ ( 𝑄 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑄 : 𝐴 ⟶ 𝐵 )
37 4 36 syl ⊢ ( 𝜑 → 𝑄 : 𝐴 ⟶ 𝐵 )
38 37 10 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 )
39 32 35 38 3jca ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 ) )
41 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) )
42 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑋 ‘ 𝑎 ) = ( 𝑋 ‘ 𝑏 ) )
43 41 42 breq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) ) )
44 8 43 syl5ibcom ⊢ ( 𝜑 → ( 𝑎 = 𝑏 → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) ) )
45 44 imp ⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) )
46 11 adantr ⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) )
47 potr ⊢ ( ( 𝑆 Po 𝐵 ∧ ( ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 ) ) → ( ( ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) ∧ ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) )
48 47 imp ⊢ ( ( ( 𝑆 Po 𝐵 ∧ ( ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 ) ) ∧ ( ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) ∧ ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) )
49 29 40 45 46 48 syl22anc ⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) )
50 ifeq1 ⊢ ( 𝑎 = 𝑏 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) = if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑏 ) )
51 ifid ⊢ if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑏 ) = 𝑏
52 50 51 eqtrdi ⊢ ( 𝑎 = 𝑏 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) = 𝑏 )
53 52 fveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑃 ‘ 𝑏 ) )
54 52 fveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑄 ‘ 𝑏 ) )
55 53 54 breq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) )
57 49 56 mpbird ⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) )
58 breq1 ⊢ ( 𝑐 = 𝑏 → ( 𝑐 𝑅 𝑎 ↔ 𝑏 𝑅 𝑎 ) )
59 fveq2 ⊢ ( 𝑐 = 𝑏 → ( 𝑃 ‘ 𝑐 ) = ( 𝑃 ‘ 𝑏 ) )
60 fveq2 ⊢ ( 𝑐 = 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑏 ) )
61 59 60 eqeq12d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ↔ ( 𝑃 ‘ 𝑏 ) = ( 𝑋 ‘ 𝑏 ) ) )
62 58 61 imbi12d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ↔ ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑋 ‘ 𝑏 ) ) ) )
63 62 9 10 rspcdva ⊢ ( 𝜑 → ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑋 ‘ 𝑏 ) ) )
64 63 imp ⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( 𝑃 ‘ 𝑏 ) = ( 𝑋 ‘ 𝑏 ) )
65 11 adantr ⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) )
66 64 65 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) )
67 sopo ⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 )
68 5 67 syl ⊢ ( 𝜑 → 𝑅 Po 𝐴 )
69 po2nr ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ) → ¬ ( 𝑏 𝑅 𝑎 ∧ 𝑎 𝑅 𝑏 ) )
70 68 10 7 69 syl12anc ⊢ ( 𝜑 → ¬ ( 𝑏 𝑅 𝑎 ∧ 𝑎 𝑅 𝑏 ) )
71 nan ⊢ ( ( 𝜑 → ¬ ( 𝑏 𝑅 𝑎 ∧ 𝑎 𝑅 𝑏 ) ) ↔ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) )
72 70 71 mpbi ⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ¬ 𝑎 𝑅 𝑏 )
73 iffalse ⊢ ( ¬ 𝑎 𝑅 𝑏 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) = 𝑏 )
74 73 fveq2d ⊢ ( ¬ 𝑎 𝑅 𝑏 → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑃 ‘ 𝑏 ) )
75 73 fveq2d ⊢ ( ¬ 𝑎 𝑅 𝑏 → ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑄 ‘ 𝑏 ) )
76 74 75 breq12d ⊢ ( ¬ 𝑎 𝑅 𝑏 → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) )
77 72 76 syl ⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) )
78 66 77 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) )
79 solin ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) )
80 5 7 10 79 syl12anc ⊢ ( 𝜑 → ( 𝑎 𝑅 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) )
81 28 57 78 80 mpjao3dan ⊢ ( 𝜑 → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) )
82 r19.26 ⊢ ( ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ↔ ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
83 9 12 82 sylanbrc ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
84 5 7 10 3jca ⊢ ( 𝜑 → ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) )
85 anim12 ⊢ ( ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ∧ ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
86 eqtr ⊢ ( ( ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ∧ ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) )
87 85 86 syl6 ⊢ ( ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) )
88 87 ralimi ⊢ ( ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) )
89 simpl1 ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑅 Or 𝐴 )
90 simpr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ 𝐴 )
91 simpl2 ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
92 simpl3 ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑏 ∈ 𝐴 )
93 soltmin ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ↔ ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) ) )
94 89 90 91 92 93 syl13anc ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ↔ ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) ) )
95 94 biimpd ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) ) )
96 95 imim1d ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → ( ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) → ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
97 96 ralimdva ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
98 84 88 97 syl2im ⊢ ( 𝜑 → ( ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
99 83 98 mpd ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) )
100 fveq2 ⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑑 ) = ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) )
101 fveq2 ⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑄 ‘ 𝑑 ) = ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) )
102 100 101 breq12d ⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ↔ ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ) )
103 breq2 ⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑐 𝑅 𝑑 ↔ 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) )
104 103 imbi1d ⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ↔ ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
105 104 ralbidv ⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ↔ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
106 102 105 anbi12d ⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ↔ ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) )
107 106 rspcev ⊢ ( ( if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ∈ 𝐴 ∧ ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) → ∃ 𝑑 ∈ 𝐴 ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
108 13 81 99 107 syl12anc ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐴 ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) )
109 1 wemaplem1 ⊢ ( ( 𝑃 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑄 ∈ ( 𝐵 ↑m 𝐴 ) ) → ( 𝑃 𝑇 𝑄 ↔ ∃ 𝑑 ∈ 𝐴 ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) )
110 2 4 109 syl2anc ⊢ ( 𝜑 → ( 𝑃 𝑇 𝑄 ↔ ∃ 𝑑 ∈ 𝐴 ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) )
111 108 110 mpbird ⊢ ( 𝜑 → 𝑃 𝑇 𝑄 )