MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unxpwdom2 Structured version   Visualization version   GIF version

Theorem unxpwdom2 9229
Description: Lemma for unxpwdom 9230. (Contributed by Mario Carneiro, 15-May-2015.)
Assertion
Ref Expression
unxpwdom2 ((𝐴 × 𝐴) ≈ (𝐵𝐶) → (𝐴* 𝐵𝐴𝐶))

Proof of Theorem unxpwdom2
Dummy variables 𝑥 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ensym 8700 . 2 ((𝐴 × 𝐴) ≈ (𝐵𝐶) → (𝐵𝐶) ≈ (𝐴 × 𝐴))
2 bren 8657 . . 3 ((𝐵𝐶) ≈ (𝐴 × 𝐴) ↔ ∃𝑓 𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴))
3 ssdif0 4293 . . . . . 6 (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ↔ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅)
4 dmxpid 5814 . . . . . . . . . . . . . 14 dom (𝐴 × 𝐴) = 𝐴
5 f1ofo 6687 . . . . . . . . . . . . . . . . 17 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵𝐶)–onto→(𝐴 × 𝐴))
6 forn 6655 . . . . . . . . . . . . . . . . 17 (𝑓:(𝐵𝐶)–onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
75, 6syl 17 . . . . . . . . . . . . . . . 16 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
8 vex 3425 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
98rnex 7709 . . . . . . . . . . . . . . . 16 ran 𝑓 ∈ V
107, 9eqeltrrdi 2848 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 × 𝐴) ∈ V)
1110dmexd 7702 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → dom (𝐴 × 𝐴) ∈ V)
124, 11eqeltrrid 2844 . . . . . . . . . . . . 13 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐴 ∈ V)
13 imassrn 5955 . . . . . . . . . . . . . 14 (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ ran ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)
14 f1stres 7804 . . . . . . . . . . . . . . . 16 (1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴
15 f1of 6680 . . . . . . . . . . . . . . . 16 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴))
16 fco 6588 . . . . . . . . . . . . . . . 16 (((1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵𝐶)⟶𝐴)
1714, 15, 16sylancr 590 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵𝐶)⟶𝐴)
1817frnd 6572 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ran ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ⊆ 𝐴)
1913, 18sstrid 3927 . . . . . . . . . . . . 13 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ 𝐴)
2012, 19ssexd 5232 . . . . . . . . . . . 12 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
2120adantr 484 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
22 simpr 488 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
23 ssdomg 8697 . . . . . . . . . . 11 ((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
2421, 22, 23sylc 65 . . . . . . . . . 10 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
25 domwdom 9215 . . . . . . . . . 10 (𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
2624, 25syl 17 . . . . . . . . 9 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
2717ffund 6568 . . . . . . . . . . 11 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → Fun ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓))
28 ssun1 4101 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵𝐶)
29 f1odm 6684 . . . . . . . . . . . . 13 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → dom 𝑓 = (𝐵𝐶))
308dmex 7708 . . . . . . . . . . . . 13 dom 𝑓 ∈ V
3129, 30eqeltrrdi 2848 . . . . . . . . . . . 12 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐵𝐶) ∈ V)
32 ssexg 5231 . . . . . . . . . . . 12 ((𝐵 ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ∈ V) → 𝐵 ∈ V)
3328, 31, 32sylancr 590 . . . . . . . . . . 11 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐵 ∈ V)
34 wdomima2g 9227 . . . . . . . . . . 11 ((Fun ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ∧ 𝐵 ∈ V ∧ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
3527, 33, 20, 34syl3anc 1373 . . . . . . . . . 10 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
3635adantr 484 . . . . . . . . 9 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
37 wdomtr 9216 . . . . . . . . 9 ((𝐴* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∧ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵) → 𝐴* 𝐵)
3826, 36, 37syl2anc 587 . . . . . . . 8 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴* 𝐵)
3938orcd 873 . . . . . . 7 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴* 𝐵𝐴𝐶))
4039ex 416 . . . . . 6 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → (𝐴* 𝐵𝐴𝐶)))
413, 40syl5bir 246 . . . . 5 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅ → (𝐴* 𝐵𝐴𝐶)))
42 n0 4276 . . . . . 6 ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
43 ssun2 4102 . . . . . . . . . . . . 13 𝐶 ⊆ (𝐵𝐶)
44 ssexg 5231 . . . . . . . . . . . . 13 ((𝐶 ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ∈ V) → 𝐶 ∈ V)
4543, 31, 44sylancr 590 . . . . . . . . . . . 12 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐶 ∈ V)
4645adantr 484 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐶 ∈ V)
47 f1ofn 6681 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓 Fn (𝐵𝐶))
48 elpreima 6897 . . . . . . . . . . . . . . 15 (𝑓 Fn (𝐵𝐶) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴))))
4947, 48syl 17 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴))))
5049adantr 484 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴))))
51 elun 4078 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝐵𝐶) ↔ (𝑦𝐵𝑦𝐶))
52 df-or 848 . . . . . . . . . . . . . . . 16 ((𝑦𝐵𝑦𝐶) ↔ (¬ 𝑦𝐵𝑦𝐶))
5351, 52bitri 278 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐵𝐶) ↔ (¬ 𝑦𝐵𝑦𝐶))
54 eldifn 4057 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
5554ad2antlr 727 . . . . . . . . . . . . . . . . . 18 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
5615ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴))
57 simprr 773 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑦𝐵)
5828, 57sselid 3913 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑦 ∈ (𝐵𝐶))
59 fvco3 6829 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴) ∧ 𝑦 ∈ (𝐵𝐶)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)))
6056, 58, 59syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)))
61 eldifi 4056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝑥𝐴)
6261adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝑥𝐴)
6362snssd 4737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → {𝑥} ⊆ 𝐴)
64 xpss1 5585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑥} ⊆ 𝐴 → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
6665adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
67 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (𝑓𝑦) ∈ ({𝑥} × 𝐴))
6866, 67sseldd 3917 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (𝑓𝑦) ∈ (𝐴 × 𝐴))
6968fvresd 6756 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = (1st ‘(𝑓𝑦)))
70 xp1st 7812 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → (1st ‘(𝑓𝑦)) ∈ {𝑥})
7167, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (1st ‘(𝑓𝑦)) ∈ {𝑥})
7269, 71eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) ∈ {𝑥})
73 elsni 4573 . . . . . . . . . . . . . . . . . . . . . 22 (((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) ∈ {𝑥} → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = 𝑥)
7472, 73syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = 𝑥)
7560, 74eqtrd 2778 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = 𝑥)
7617ffnd 6565 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵𝐶))
7776ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵𝐶))
7828a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝐵 ⊆ (𝐵𝐶))
79 fnfvima 7068 . . . . . . . . . . . . . . . . . . . . 21 ((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵𝐶) ∧ 𝐵 ⊆ (𝐵𝐶) ∧ 𝑦𝐵) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
8077, 78, 57, 79syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
8175, 80eqeltrrd 2840 . . . . . . . . . . . . . . . . . . 19 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
8281expr 460 . . . . . . . . . . . . . . . . . 18 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → (𝑦𝐵𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
8355, 82mtod 201 . . . . . . . . . . . . . . . . 17 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑦𝐵)
8483ex 416 . . . . . . . . . . . . . . . 16 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → ¬ 𝑦𝐵))
8584imim1d 82 . . . . . . . . . . . . . . 15 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((¬ 𝑦𝐵𝑦𝐶) → ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → 𝑦𝐶)))
8653, 85syl5bi 245 . . . . . . . . . . . . . 14 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝐵𝐶) → ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → 𝑦𝐶)))
8786impd 414 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → 𝑦𝐶))
8850, 87sylbid 243 . . . . . . . . . . . 12 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) → 𝑦𝐶))
8988ssrdv 3922 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶)
90 ssdomg 8697 . . . . . . . . . . 11 (𝐶 ∈ V → ((𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶 → (𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶))
9146, 89, 90sylc 65 . . . . . . . . . 10 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶)
92 f1ocnv 6692 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵𝐶))
93 f1of1 6679 . . . . . . . . . . . . . . 15 (𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵𝐶) → 𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶))
9492, 93syl 17 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶))
9594adantr 484 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶))
9631adantr 484 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐵𝐶) ∈ V)
97 snex 5339 . . . . . . . . . . . . . 14 {𝑥} ∈ V
9812adantr 484 . . . . . . . . . . . . . 14 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴 ∈ V)
99 xpexg 7554 . . . . . . . . . . . . . 14 (({𝑥} ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ∈ V)
10097, 98, 99sylancr 590 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ∈ V)
101 f1imaen2g 8712 . . . . . . . . . . . . 13 (((𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶) ∧ (𝐵𝐶) ∈ V) ∧ (({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴) ∧ ({𝑥} × 𝐴) ∈ V)) → (𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
10295, 96, 65, 100, 101syl22anc 839 . . . . . . . . . . . 12 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
103 vex 3425 . . . . . . . . . . . . 13 𝑥 ∈ V
104 xpsnen2g 8761 . . . . . . . . . . . . 13 ((𝑥 ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ≈ 𝐴)
105103, 98, 104sylancr 590 . . . . . . . . . . . 12 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ≈ 𝐴)
106 entr 8703 . . . . . . . . . . . 12 (((𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴) ∧ ({𝑥} × 𝐴) ≈ 𝐴) → (𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
107102, 105, 106syl2anc 587 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
108 domen1 8811 . . . . . . . . . . 11 ((𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴 → ((𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶𝐴𝐶))
109107, 108syl 17 . . . . . . . . . 10 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶𝐴𝐶))
11091, 109mpbid 235 . . . . . . . . 9 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴𝐶)
111110olcd 874 . . . . . . . 8 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐴* 𝐵𝐴𝐶))
112111ex 416 . . . . . . 7 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴* 𝐵𝐴𝐶)))
113112exlimdv 1941 . . . . . 6 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴* 𝐵𝐴𝐶)))
11442, 113syl5bi 245 . . . . 5 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ → (𝐴* 𝐵𝐴𝐶)))
11541, 114pm2.61dne 3029 . . . 4 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴* 𝐵𝐴𝐶))
116115exlimiv 1938 . . 3 (∃𝑓 𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴* 𝐵𝐴𝐶))
1172, 116sylbi 220 . 2 ((𝐵𝐶) ≈ (𝐴 × 𝐴) → (𝐴* 𝐵𝐴𝐶))
1181, 117syl 17 1 ((𝐴 × 𝐴) ≈ (𝐵𝐶) → (𝐴* 𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847   = wceq 1543  wex 1787  wcel 2111  wne 2941  Vcvv 3421  cdif 3878  cun 3879  wss 3881  c0 4252  {csn 4556   class class class wbr 5068   × cxp 5564  ccnv 5565  dom cdm 5566  ran crn 5567  cres 5568  cima 5569  ccom 5570  Fun wfun 6392   Fn wfn 6393  wf 6394  1-1wf1 6395  ontowfo 6396  1-1-ontowf1o 6397  cfv 6398  1st c1st 7778  cen 8644  cdom 8645  * cwdom 9205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5207  ax-nul 5214  ax-pow 5273  ax-pr 5337  ax-un 7542
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3423  df-sbc 3710  df-csb 3827  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4253  df-if 4455  df-pw 4530  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4835  df-int 4875  df-iun 4921  df-br 5069  df-opab 5131  df-mpt 5151  df-id 5470  df-xp 5572  df-rel 5573  df-cnv 5574  df-co 5575  df-dm 5576  df-rn 5577  df-res 5578  df-ima 5579  df-iota 6356  df-fun 6400  df-fn 6401  df-f 6402  df-f1 6403  df-fo 6404  df-f1o 6405  df-fv 6406  df-1st 7780  df-2nd 7781  df-er 8412  df-en 8648  df-dom 8649  df-sdom 8650  df-wdom 9206
This theorem is referenced by:  unxpwdom  9230  ttac  40594
  Copyright terms: Public domain W3C validator