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 sseldi ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) )
15 elmapi ⊢ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑎 : 𝐴 ⟶ 𝐵 )
16 14 15 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 : 𝐴 ⟶ 𝐵 )
17 16 ffnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 Fn 𝐴 )
18 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑏 ∈ 𝑈 )
19 2 18 sseldi ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑏 ∈ ( 𝐵 ↑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 𝑈 )