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 ffvelrnd ( 𝜑 → ( 𝑃𝑏 ) ∈ 𝐵 )
33 elmapi ( 𝑋 ∈ ( 𝐵m 𝐴 ) → 𝑋 : 𝐴𝐵 )
34 3 33 syl ( 𝜑𝑋 : 𝐴𝐵 )
35 34 10 ffvelrnd ( 𝜑 → ( 𝑋𝑏 ) ∈ 𝐵 )
36 elmapi ( 𝑄 ∈ ( 𝐵m 𝐴 ) → 𝑄 : 𝐴𝐵 )
37 4 36 syl ( 𝜑𝑄 : 𝐴𝐵 )
38 37 10 ffvelrnd ( 𝜑 → ( 𝑄𝑏 ) ∈ 𝐵 )
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 ( 𝜑𝑃 𝑇 𝑄 )