Metamath Proof Explorer


Theorem wemapsolem

Description: Lemma for wemapso . (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Mario Carneiro, 8-Feb-2015) (Revised by AV, 21-Jul-2024)

Ref Expression
Hypotheses wemapso.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐴 ( ( 𝑥𝑧 ) 𝑆 ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
wemapsolem.1 𝑈 ⊆ ( 𝐵m 𝐴 )
wemapsolem.2 ( 𝜑𝑅 Or 𝐴 )
wemapsolem.3 ( 𝜑𝑆 Or 𝐵 )
wemapsolem.4 ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ∃ 𝑐 ∈ dom ( 𝑎𝑏 ) ∀ 𝑑 ∈ dom ( 𝑎𝑏 ) ¬ 𝑑 𝑅 𝑐 )
Assertion wemapsolem ( 𝜑𝑇 Or 𝑈 )

Proof

Step Hyp Ref Expression
1 wemapso.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐴 ( ( 𝑥𝑧 ) 𝑆 ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
2 wemapsolem.1 𝑈 ⊆ ( 𝐵m 𝐴 )
3 wemapsolem.2 ( 𝜑𝑅 Or 𝐴 )
4 wemapsolem.3 ( 𝜑𝑆 Or 𝐵 )
5 wemapsolem.4 ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ∃ 𝑐 ∈ dom ( 𝑎𝑏 ) ∀ 𝑑 ∈ dom ( 𝑎𝑏 ) ¬ 𝑑 𝑅 𝑐 )
6 sopo ( 𝑆 Or 𝐵𝑆 Po 𝐵 )
7 4 6 syl ( 𝜑𝑆 Po 𝐵 )
8 1 wemappo ( ( 𝑅 Or 𝐴𝑆 Po 𝐵 ) → 𝑇 Po ( 𝐵m 𝐴 ) )
9 3 7 8 syl2anc ( 𝜑𝑇 Po ( 𝐵m 𝐴 ) )
10 poss ( 𝑈 ⊆ ( 𝐵m 𝐴 ) → ( 𝑇 Po ( 𝐵m 𝐴 ) → 𝑇 Po 𝑈 ) )
11 2 9 10 mpsyl ( 𝜑𝑇 Po 𝑈 )
12 df-ne ( 𝑎𝑏 ↔ ¬ 𝑎 = 𝑏 )
13 simprll ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → 𝑎𝑈 )
14 2 13 sselid ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → 𝑎 ∈ ( 𝐵m 𝐴 ) )
15 elmapi ( 𝑎 ∈ ( 𝐵m 𝐴 ) → 𝑎 : 𝐴𝐵 )
16 14 15 syl ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → 𝑎 : 𝐴𝐵 )
17 16 ffnd ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → 𝑎 Fn 𝐴 )
18 simprlr ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → 𝑏𝑈 )
19 2 18 sselid ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → 𝑏 ∈ ( 𝐵m 𝐴 ) )
20 elmapi ( 𝑏 ∈ ( 𝐵m 𝐴 ) → 𝑏 : 𝐴𝐵 )
21 19 20 syl ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → 𝑏 : 𝐴𝐵 )
22 21 ffnd ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → 𝑏 Fn 𝐴 )
23 fndmdif ( ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) → dom ( 𝑎𝑏 ) = { 𝑥𝐴 ∣ ( 𝑎𝑥 ) ≠ ( 𝑏𝑥 ) } )
24 17 22 23 syl2anc ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → dom ( 𝑎𝑏 ) = { 𝑥𝐴 ∣ ( 𝑎𝑥 ) ≠ ( 𝑏𝑥 ) } )
25 24 eleq2d ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( 𝑐 ∈ dom ( 𝑎𝑏 ) ↔ 𝑐 ∈ { 𝑥𝐴 ∣ ( 𝑎𝑥 ) ≠ ( 𝑏𝑥 ) } ) )
26 nesym ( ( 𝑎𝑥 ) ≠ ( 𝑏𝑥 ) ↔ ¬ ( 𝑏𝑥 ) = ( 𝑎𝑥 ) )
27 fveq2 ( 𝑥 = 𝑐 → ( 𝑏𝑥 ) = ( 𝑏𝑐 ) )
28 fveq2 ( 𝑥 = 𝑐 → ( 𝑎𝑥 ) = ( 𝑎𝑐 ) )
29 27 28 eqeq12d ( 𝑥 = 𝑐 → ( ( 𝑏𝑥 ) = ( 𝑎𝑥 ) ↔ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ) )
30 29 notbid ( 𝑥 = 𝑐 → ( ¬ ( 𝑏𝑥 ) = ( 𝑎𝑥 ) ↔ ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ) )
31 26 30 syl5bb ( 𝑥 = 𝑐 → ( ( 𝑎𝑥 ) ≠ ( 𝑏𝑥 ) ↔ ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ) )
32 31 elrab ( 𝑐 ∈ { 𝑥𝐴 ∣ ( 𝑎𝑥 ) ≠ ( 𝑏𝑥 ) } ↔ ( 𝑐𝐴 ∧ ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ) )
33 25 32 bitrdi ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( 𝑐 ∈ dom ( 𝑎𝑏 ) ↔ ( 𝑐𝐴 ∧ ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ) ) )
34 24 eleq2d ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( 𝑑 ∈ dom ( 𝑎𝑏 ) ↔ 𝑑 ∈ { 𝑥𝐴 ∣ ( 𝑎𝑥 ) ≠ ( 𝑏𝑥 ) } ) )
35 fveq2 ( 𝑥 = 𝑑 → ( 𝑏𝑥 ) = ( 𝑏𝑑 ) )
36 fveq2 ( 𝑥 = 𝑑 → ( 𝑎𝑥 ) = ( 𝑎𝑑 ) )
37 35 36 eqeq12d ( 𝑥 = 𝑑 → ( ( 𝑏𝑥 ) = ( 𝑎𝑥 ) ↔ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) )
38 37 notbid ( 𝑥 = 𝑑 → ( ¬ ( 𝑏𝑥 ) = ( 𝑎𝑥 ) ↔ ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) )
39 26 38 syl5bb ( 𝑥 = 𝑑 → ( ( 𝑎𝑥 ) ≠ ( 𝑏𝑥 ) ↔ ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) )
40 39 elrab ( 𝑑 ∈ { 𝑥𝐴 ∣ ( 𝑎𝑥 ) ≠ ( 𝑏𝑥 ) } ↔ ( 𝑑𝐴 ∧ ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) )
41 34 40 bitrdi ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( 𝑑 ∈ dom ( 𝑎𝑏 ) ↔ ( 𝑑𝐴 ∧ ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) )
42 41 imbi1d ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( ( 𝑑 ∈ dom ( 𝑎𝑏 ) → ¬ 𝑑 𝑅 𝑐 ) ↔ ( ( 𝑑𝐴 ∧ ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) → ¬ 𝑑 𝑅 𝑐 ) ) )
43 impexp ( ( ( 𝑑𝐴 ∧ ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) → ¬ 𝑑 𝑅 𝑐 ) ↔ ( 𝑑𝐴 → ( ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) → ¬ 𝑑 𝑅 𝑐 ) ) )
44 con34b ( ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ↔ ( ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) → ¬ 𝑑 𝑅 𝑐 ) )
45 44 imbi2i ( ( 𝑑𝐴 → ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ↔ ( 𝑑𝐴 → ( ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) → ¬ 𝑑 𝑅 𝑐 ) ) )
46 43 45 bitr4i ( ( ( 𝑑𝐴 ∧ ¬ ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) → ¬ 𝑑 𝑅 𝑐 ) ↔ ( 𝑑𝐴 → ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) )
47 42 46 bitrdi ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( ( 𝑑 ∈ dom ( 𝑎𝑏 ) → ¬ 𝑑 𝑅 𝑐 ) ↔ ( 𝑑𝐴 → ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) )
48 47 ralbidv2 ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( ∀ 𝑑 ∈ dom ( 𝑎𝑏 ) ¬ 𝑑 𝑅 𝑐 ↔ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) )
49 33 48 anbi12d ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( ( 𝑐 ∈ dom ( 𝑎𝑏 ) ∧ ∀ 𝑑 ∈ dom ( 𝑎𝑏 ) ¬ 𝑑 𝑅 𝑐 ) ↔ ( ( 𝑐𝐴 ∧ ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) )
50 anass ( ( ( 𝑐𝐴 ∧ ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ↔ ( 𝑐𝐴 ∧ ( ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) )
51 49 50 bitrdi ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( ( 𝑐 ∈ dom ( 𝑎𝑏 ) ∧ ∀ 𝑑 ∈ dom ( 𝑎𝑏 ) ¬ 𝑑 𝑅 𝑐 ) ↔ ( 𝑐𝐴 ∧ ( ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) ) )
52 51 rexbidv2 ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( ∃ 𝑐 ∈ dom ( 𝑎𝑏 ) ∀ 𝑑 ∈ dom ( 𝑎𝑏 ) ¬ 𝑑 𝑅 𝑐 ↔ ∃ 𝑐𝐴 ( ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) )
53 5 52 mpbid ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ∃ 𝑐𝐴 ( ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) )
54 4 ad2antrr ( ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) ∧ 𝑐𝐴 ) → 𝑆 Or 𝐵 )
55 21 ffvelrnda ( ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) ∧ 𝑐𝐴 ) → ( 𝑏𝑐 ) ∈ 𝐵 )
56 16 ffvelrnda ( ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) ∧ 𝑐𝐴 ) → ( 𝑎𝑐 ) ∈ 𝐵 )
57 sotrieq ( ( 𝑆 Or 𝐵 ∧ ( ( 𝑏𝑐 ) ∈ 𝐵 ∧ ( 𝑎𝑐 ) ∈ 𝐵 ) ) → ( ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ↔ ¬ ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ) )
58 57 con2bid ( ( 𝑆 Or 𝐵 ∧ ( ( 𝑏𝑐 ) ∈ 𝐵 ∧ ( 𝑎𝑐 ) ∈ 𝐵 ) ) → ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ↔ ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ) )
59 58 biimprd ( ( 𝑆 Or 𝐵 ∧ ( ( 𝑏𝑐 ) ∈ 𝐵 ∧ ( 𝑎𝑐 ) ∈ 𝐵 ) ) → ( ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) → ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ) )
60 54 55 56 59 syl12anc ( ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) ∧ 𝑐𝐴 ) → ( ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) → ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ) )
61 60 anim1d ( ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) ∧ 𝑐𝐴 ) → ( ( ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) → ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) )
62 61 reximdva ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( ∃ 𝑐𝐴 ( ¬ ( 𝑏𝑐 ) = ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) → ∃ 𝑐𝐴 ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) )
63 53 62 mpd ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ∃ 𝑐𝐴 ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) )
64 1 wemaplem1 ( ( 𝑏 ∈ V ∧ 𝑎 ∈ V ) → ( 𝑏 𝑇 𝑎 ↔ ∃ 𝑐𝐴 ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) )
65 64 el2v ( 𝑏 𝑇 𝑎 ↔ ∃ 𝑐𝐴 ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) )
66 1 wemaplem1 ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( 𝑎 𝑇 𝑏 ↔ ∃ 𝑐𝐴 ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) ) ) )
67 66 el2v ( 𝑎 𝑇 𝑏 ↔ ∃ 𝑐𝐴 ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) ) )
68 65 67 orbi12i ( ( 𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) ↔ ( ∃ 𝑐𝐴 ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ∨ ∃ 𝑐𝐴 ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) ) ) )
69 r19.43 ( ∃ 𝑐𝐴 ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ∨ ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) ) ) ↔ ( ∃ 𝑐𝐴 ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ∨ ∃ 𝑐𝐴 ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) ) ) )
70 andir ( ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ↔ ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ∨ ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) )
71 eqcom ( ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ↔ ( 𝑎𝑑 ) = ( 𝑏𝑑 ) )
72 71 imbi2i ( ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ↔ ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) )
73 72 ralbii ( ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ↔ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) )
74 73 anbi2i ( ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ↔ ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) ) )
75 74 orbi2i ( ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ∨ ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ) ↔ ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ∨ ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) ) ) )
76 70 75 bitr2i ( ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ∨ ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) ) ) ↔ ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) )
77 76 rexbii ( ∃ 𝑐𝐴 ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) ∨ ( ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑎𝑑 ) = ( 𝑏𝑑 ) ) ) ) ↔ ∃ 𝑐𝐴 ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) )
78 68 69 77 3bitr2i ( ( 𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) ↔ ∃ 𝑐𝐴 ( ( ( 𝑏𝑐 ) 𝑆 ( 𝑎𝑐 ) ∨ ( 𝑎𝑐 ) 𝑆 ( 𝑏𝑐 ) ) ∧ ∀ 𝑑𝐴 ( 𝑑 𝑅 𝑐 → ( 𝑏𝑑 ) = ( 𝑎𝑑 ) ) ) )
79 63 78 sylibr ( ( 𝜑 ∧ ( ( 𝑎𝑈𝑏𝑈 ) ∧ 𝑎𝑏 ) ) → ( 𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) )
80 79 expr ( ( 𝜑 ∧ ( 𝑎𝑈𝑏𝑈 ) ) → ( 𝑎𝑏 → ( 𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) ) )
81 12 80 syl5bir ( ( 𝜑 ∧ ( 𝑎𝑈𝑏𝑈 ) ) → ( ¬ 𝑎 = 𝑏 → ( 𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) ) )
82 81 orrd ( ( 𝜑 ∧ ( 𝑎𝑈𝑏𝑈 ) ) → ( 𝑎 = 𝑏 ∨ ( 𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) ) )
83 3orrot ( ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) ↔ ( 𝑎 = 𝑏𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) )
84 3orass ( ( 𝑎 = 𝑏𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) ↔ ( 𝑎 = 𝑏 ∨ ( 𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) ) )
85 83 84 bitr2i ( ( 𝑎 = 𝑏 ∨ ( 𝑏 𝑇 𝑎𝑎 𝑇 𝑏 ) ) ↔ ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )
86 82 85 sylib ( ( 𝜑 ∧ ( 𝑎𝑈𝑏𝑈 ) ) → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )
87 11 86 issod ( 𝜑𝑇 Or 𝑈 )