Metamath Proof Explorer

Theorem unxpwdom2

Description: Lemma for unxpwdom . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion unxpwdom2 ( ( 𝐴 × 𝐴 ) ≈ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ensym ⊢ ( ( 𝐴 × 𝐴 ) ≈ ( 𝐵 ∪ 𝐶 ) → ( 𝐵 ∪ 𝐶 ) ≈ ( 𝐴 × 𝐴 ) )
2 bren ⊢ ( ( 𝐵 ∪ 𝐶 ) ≈ ( 𝐴 × 𝐴 ) ↔ ∃ 𝑓 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) )
3 ssdif0 ⊢ ( 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ↔ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) = ∅ )
4 dmxpid ⊢ dom ( 𝐴 × 𝐴 ) = 𝐴
5 f1ofo ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → 𝑓 : ( 𝐵 ∪ 𝐶 ) –onto→ ( 𝐴 × 𝐴 ) )
6 forn ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –onto→ ( 𝐴 × 𝐴 ) → ran 𝑓 = ( 𝐴 × 𝐴 ) )
7 5 6 syl ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ran 𝑓 = ( 𝐴 × 𝐴 ) )
8 vex ⊢ 𝑓 ∈ V
9 8 rnex ⊢ ran 𝑓 ∈ V
10 7 9 eqeltrrdi ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( 𝐴 × 𝐴 ) ∈ V )
11 10 dmexd ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → dom ( 𝐴 × 𝐴 ) ∈ V )
12 4 11 eqeltrrid ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → 𝐴 ∈ V )
13 imassrn ⊢ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ⊆ ran ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 )
14 f1stres ⊢ ( 1st ↾ ( 𝐴 × 𝐴 ) ) : ( 𝐴 × 𝐴 ) ⟶ 𝐴
15 f1of ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → 𝑓 : ( 𝐵 ∪ 𝐶 ) ⟶ ( 𝐴 × 𝐴 ) )
16 fco ⊢ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) : ( 𝐴 × 𝐴 ) ⟶ 𝐴 ∧ 𝑓 : ( 𝐵 ∪ 𝐶 ) ⟶ ( 𝐴 × 𝐴 ) ) → ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) : ( 𝐵 ∪ 𝐶 ) ⟶ 𝐴 )
17 14 15 16 sylancr ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) : ( 𝐵 ∪ 𝐶 ) ⟶ 𝐴 )
18 17 frnd ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ran ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) ⊆ 𝐴 )
19 13 18 sstrid ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ⊆ 𝐴 )
20 12 19 ssexd ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ∈ V )
21 20 adantr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ∈ V )
22 simpr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) )
23 ssdomg ⊢ ( ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ∈ V → ( 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) → 𝐴 ≼ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) )
24 21 22 23 sylc ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → 𝐴 ≼ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) )
25 domwdom ⊢ ( 𝐴 ≼ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) → 𝐴 ≼* ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) )
26 24 25 syl ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → 𝐴 ≼* ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) )
27 17 ffund ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → Fun ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) )
28 ssun1 ⊢ 𝐵 ⊆ ( 𝐵 ∪ 𝐶 )
29 f1odm ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → dom 𝑓 = ( 𝐵 ∪ 𝐶 ) )
30 8 dmex ⊢ dom 𝑓 ∈ V
31 29 30 eqeltrrdi ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( 𝐵 ∪ 𝐶 ) ∈ V )
32 ssexg ⊢ ( ( 𝐵 ⊆ ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐵 ∪ 𝐶 ) ∈ V ) → 𝐵 ∈ V )
33 28 31 32 sylancr ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → 𝐵 ∈ V )
34 wdomima2g ⊢ ( ( Fun ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) ∧ 𝐵 ∈ V ∧ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ∈ V ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ≼* 𝐵 )
35 27 33 20 34 syl3anc ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ≼* 𝐵 )
36 35 adantr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ≼* 𝐵 )
37 wdomtr ⊢ ( ( 𝐴 ≼* ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ∧ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ≼* 𝐵 ) → 𝐴 ≼* 𝐵 )
38 26 36 37 syl2anc ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → 𝐴 ≼* 𝐵 )
39 38 orcd ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )
40 39 ex ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( 𝐴 ⊆ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) ) )
41 3 40 syl5bir ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) = ∅ → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) ) )
42 n0 ⊢ ( ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) )
43 ssun2 ⊢ 𝐶 ⊆ ( 𝐵 ∪ 𝐶 )
44 ssexg ⊢ ( ( 𝐶 ⊆ ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐵 ∪ 𝐶 ) ∈ V ) → 𝐶 ∈ V )
45 43 31 44 sylancr ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → 𝐶 ∈ V )
46 45 adantr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → 𝐶 ∈ V )
47 f1ofn ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → 𝑓 Fn ( 𝐵 ∪ 𝐶 ) )
48 elpreima ⊢ ( 𝑓 Fn ( 𝐵 ∪ 𝐶 ) → ( 𝑦 ∈ ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ↔ ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ) ) )
49 47 48 syl ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( 𝑦 ∈ ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ↔ ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ) ) )
50 49 adantr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( 𝑦 ∈ ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ↔ ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ) ) )
51 elun ⊢ ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) )
52 df-or ⊢ ( ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) ↔ ( ¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
53 51 52 bitri ⊢ ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( ¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
54 eldifn ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → ¬ 𝑥 ∈ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) )
55 54 ad2antlr ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ) → ¬ 𝑥 ∈ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) )
56 15 ad2antrr ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑓 : ( 𝐵 ∪ 𝐶 ) ⟶ ( 𝐴 × 𝐴 ) )
57 simprr ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
58 28 57 sselid ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) )
59 fvco3 ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) ⟶ ( 𝐴 × 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) ‘ 𝑦 ) = ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ‘ ( 𝑓 ‘ 𝑦 ) ) )
60 56 58 59 syl2anc ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) ‘ 𝑦 ) = ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ‘ ( 𝑓 ‘ 𝑦 ) ) )
61 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → 𝑥 ∈ 𝐴 )
62 61 adantl ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → 𝑥 ∈ 𝐴 )
63 62 snssd ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → { 𝑥 } ⊆ 𝐴 )
64 xpss1 ⊢ ( { 𝑥 } ⊆ 𝐴 → ( { 𝑥 } × 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) )
65 63 64 syl ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( { 𝑥 } × 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) )
66 65 adantr ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑥 } × 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) )
67 simprl ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) )
68 66 67 sseldd ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝐴 × 𝐴 ) )
69 68 fvresd ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ‘ ( 𝑓 ‘ 𝑦 ) ) = ( 1st ‘ ( 𝑓 ‘ 𝑦 ) ) )
70 xp1st ⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) → ( 1st ‘ ( 𝑓 ‘ 𝑦 ) ) ∈ { 𝑥 } )
71 67 70 syl ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 1st ‘ ( 𝑓 ‘ 𝑦 ) ) ∈ { 𝑥 } )
72 69 71 eqeltrd ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ‘ ( 𝑓 ‘ 𝑦 ) ) ∈ { 𝑥 } )
73 elsni ⊢ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ‘ ( 𝑓 ‘ 𝑦 ) ) ∈ { 𝑥 } → ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ‘ ( 𝑓 ‘ 𝑦 ) ) = 𝑥 )
74 72 73 syl ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ‘ ( 𝑓 ‘ 𝑦 ) ) = 𝑥 )
75 60 74 eqtrd ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) ‘ 𝑦 ) = 𝑥 )
76 17 ffnd ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) Fn ( 𝐵 ∪ 𝐶 ) )
77 76 ad2antrr ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) Fn ( 𝐵 ∪ 𝐶 ) )
78 28 a1i ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝐵 ⊆ ( 𝐵 ∪ 𝐶 ) )
79 fnfvima ⊢ ( ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) Fn ( 𝐵 ∪ 𝐶 ) ∧ 𝐵 ⊆ ( 𝐵 ∪ 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) ‘ 𝑦 ) ∈ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) )
80 77 78 57 79 syl3anc ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) ‘ 𝑦 ) ∈ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) )
81 75 80 eqeltrrd ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) )
82 81 expr ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ) → ( 𝑦 ∈ 𝐵 → 𝑥 ∈ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) )
83 55 82 mtod ⊢ ( ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ) → ¬ 𝑦 ∈ 𝐵 )
84 83 ex ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) → ¬ 𝑦 ∈ 𝐵 ) )
85 84 imim1d ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( ( ¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) → ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) → 𝑦 ∈ 𝐶 ) ) )
86 53 85 syl5bi ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) → ( ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) → 𝑦 ∈ 𝐶 ) ) )
87 86 impd ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( { 𝑥 } × 𝐴 ) ) → 𝑦 ∈ 𝐶 ) )
88 50 87 sylbid ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( 𝑦 ∈ ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) → 𝑦 ∈ 𝐶 ) )
89 88 ssrdv ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ⊆ 𝐶 )
90 ssdomg ⊢ ( 𝐶 ∈ V → ( ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ⊆ 𝐶 → ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≼ 𝐶 ) )
91 46 89 90 sylc ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≼ 𝐶 )
92 f1ocnv ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ◡ 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ ( 𝐵 ∪ 𝐶 ) )
93 f1of1 ⊢ ( ◡ 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ ( 𝐵 ∪ 𝐶 ) → ◡ 𝑓 : ( 𝐴 × 𝐴 ) –1-1→ ( 𝐵 ∪ 𝐶 ) )
94 92 93 syl ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ◡ 𝑓 : ( 𝐴 × 𝐴 ) –1-1→ ( 𝐵 ∪ 𝐶 ) )
95 94 adantr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ◡ 𝑓 : ( 𝐴 × 𝐴 ) –1-1→ ( 𝐵 ∪ 𝐶 ) )
96 31 adantr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( 𝐵 ∪ 𝐶 ) ∈ V )
97 snex ⊢ { 𝑥 } ∈ V
98 12 adantr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → 𝐴 ∈ V )
99 xpexg ⊢ ( ( { 𝑥 } ∈ V ∧ 𝐴 ∈ V ) → ( { 𝑥 } × 𝐴 ) ∈ V )
100 97 98 99 sylancr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( { 𝑥 } × 𝐴 ) ∈ V )
101 f1imaen2g ⊢ ( ( ( ◡ 𝑓 : ( 𝐴 × 𝐴 ) –1-1→ ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐵 ∪ 𝐶 ) ∈ V ) ∧ ( ( { 𝑥 } × 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) ∧ ( { 𝑥 } × 𝐴 ) ∈ V ) ) → ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≈ ( { 𝑥 } × 𝐴 ) )
102 95 96 65 100 101 syl22anc ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≈ ( { 𝑥 } × 𝐴 ) )
103 vex ⊢ 𝑥 ∈ V
104 xpsnen2g ⊢ ( ( 𝑥 ∈ V ∧ 𝐴 ∈ V ) → ( { 𝑥 } × 𝐴 ) ≈ 𝐴 )
105 103 98 104 sylancr ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( { 𝑥 } × 𝐴 ) ≈ 𝐴 )
106 entr ⊢ ( ( ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≈ ( { 𝑥 } × 𝐴 ) ∧ ( { 𝑥 } × 𝐴 ) ≈ 𝐴 ) → ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≈ 𝐴 )
107 102 105 106 syl2anc ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≈ 𝐴 )
108 domen1 ⊢ ( ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≈ 𝐴 → ( ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≼ 𝐶 ↔ 𝐴 ≼ 𝐶 ) )
109 107 108 syl ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( ( ◡ 𝑓 “ ( { 𝑥 } × 𝐴 ) ) ≼ 𝐶 ↔ 𝐴 ≼ 𝐶 ) )
110 91 109 mpbid ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → 𝐴 ≼ 𝐶 )
111 110 olcd ⊢ ( ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )
112 111 ex ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) ) )
113 112 exlimdv ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( ∃ 𝑥 𝑥 ∈ ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) ) )
114 42 113 syl5bi ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( ( 𝐴 ∖ ( ( ( 1st ↾ ( 𝐴 × 𝐴 ) ) ∘ 𝑓 ) “ 𝐵 ) ) ≠ ∅ → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) ) )
115 41 114 pm2.61dne ⊢ ( 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )
116 115 exlimiv ⊢ ( ∃ 𝑓 𝑓 : ( 𝐵 ∪ 𝐶 ) –1-1-onto→ ( 𝐴 × 𝐴 ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )
117 2 116 sylbi ⊢ ( ( 𝐵 ∪ 𝐶 ) ≈ ( 𝐴 × 𝐴 ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )
118 1 117 syl ⊢ ( ( 𝐴 × 𝐴 ) ≈ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )