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

Theorem unxpwdom2 9529
Description: Lemma for unxpwdom 9530. (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 8946 . 2 ((𝐴 × 𝐴) ≈ (𝐵𝐶) → (𝐵𝐶) ≈ (𝐴 × 𝐴))
2 bren 8896 . . 3 ((𝐵𝐶) ≈ (𝐴 × 𝐴) ↔ ∃𝑓 𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴))
3 ssdif0 4324 . . . . . 6 (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ↔ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅)
4 dmxpid 5886 . . . . . . . . . . . . . 14 dom (𝐴 × 𝐴) = 𝐴
5 f1ofo 6792 . . . . . . . . . . . . . . . . 17 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵𝐶)–onto→(𝐴 × 𝐴))
6 forn 6760 . . . . . . . . . . . . . . . . 17 (𝑓:(𝐵𝐶)–onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
75, 6syl 17 . . . . . . . . . . . . . . . 16 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
8 vex 3448 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
98rnex 7850 . . . . . . . . . . . . . . . 16 ran 𝑓 ∈ V
107, 9eqeltrrdi 2843 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 × 𝐴) ∈ V)
1110dmexd 7843 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → dom (𝐴 × 𝐴) ∈ V)
124, 11eqeltrrid 2839 . . . . . . . . . . . . 13 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐴 ∈ V)
13 imassrn 6025 . . . . . . . . . . . . . 14 (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ ran ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)
14 f1stres 7946 . . . . . . . . . . . . . . . 16 (1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴
15 f1of 6785 . . . . . . . . . . . . . . . 16 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴))
16 fco 6693 . . . . . . . . . . . . . . . 16 (((1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵𝐶)⟶𝐴)
1714, 15, 16sylancr 588 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵𝐶)⟶𝐴)
1817frnd 6677 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ran ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ⊆ 𝐴)
1913, 18sstrid 3956 . . . . . . . . . . . . 13 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ 𝐴)
2012, 19ssexd 5282 . . . . . . . . . . . 12 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
2120adantr 482 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
22 simpr 486 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
23 ssdomg 8943 . . . . . . . . . . 11 ((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
2421, 22, 23sylc 65 . . . . . . . . . 10 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
25 domwdom 9515 . . . . . . . . . 10 (𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
2624, 25syl 17 . . . . . . . . 9 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
2717ffund 6673 . . . . . . . . . . 11 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → Fun ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓))
28 ssun1 4133 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵𝐶)
29 f1odm 6789 . . . . . . . . . . . . 13 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → dom 𝑓 = (𝐵𝐶))
308dmex 7849 . . . . . . . . . . . . 13 dom 𝑓 ∈ V
3129, 30eqeltrrdi 2843 . . . . . . . . . . . 12 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐵𝐶) ∈ V)
32 ssexg 5281 . . . . . . . . . . . 12 ((𝐵 ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ∈ V) → 𝐵 ∈ V)
3328, 31, 32sylancr 588 . . . . . . . . . . 11 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐵 ∈ V)
34 wdomima2g 9527 . . . . . . . . . . 11 ((Fun ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ∧ 𝐵 ∈ V ∧ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
3527, 33, 20, 34syl3anc 1372 . . . . . . . . . 10 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
3635adantr 482 . . . . . . . . 9 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
37 wdomtr 9516 . . . . . . . . 9 ((𝐴* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∧ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵) → 𝐴* 𝐵)
3826, 36, 37syl2anc 585 . . . . . . . 8 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴* 𝐵)
3938orcd 872 . . . . . . 7 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴* 𝐵𝐴𝐶))
4039ex 414 . . . . . 6 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → (𝐴* 𝐵𝐴𝐶)))
413, 40biimtrrid 242 . . . . 5 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅ → (𝐴* 𝐵𝐴𝐶)))
42 n0 4307 . . . . . 6 ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
43 ssun2 4134 . . . . . . . . . . . . 13 𝐶 ⊆ (𝐵𝐶)
44 ssexg 5281 . . . . . . . . . . . . 13 ((𝐶 ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ∈ V) → 𝐶 ∈ V)
4543, 31, 44sylancr 588 . . . . . . . . . . . 12 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐶 ∈ V)
4645adantr 482 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐶 ∈ V)
47 f1ofn 6786 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓 Fn (𝐵𝐶))
48 elpreima 7009 . . . . . . . . . . . . . . 15 (𝑓 Fn (𝐵𝐶) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴))))
4947, 48syl 17 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴))))
5049adantr 482 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴))))
51 elun 4109 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝐵𝐶) ↔ (𝑦𝐵𝑦𝐶))
52 df-or 847 . . . . . . . . . . . . . . . 16 ((𝑦𝐵𝑦𝐶) ↔ (¬ 𝑦𝐵𝑦𝐶))
5351, 52bitri 275 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐵𝐶) ↔ (¬ 𝑦𝐵𝑦𝐶))
54 eldifn 4088 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
5554ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
5615ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴))
57 simprr 772 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑦𝐵)
5828, 57sselid 3943 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑦 ∈ (𝐵𝐶))
59 fvco3 6941 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴) ∧ 𝑦 ∈ (𝐵𝐶)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)))
6056, 58, 59syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)))
61 eldifi 4087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝑥𝐴)
6261adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝑥𝐴)
6362snssd 4770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → {𝑥} ⊆ 𝐴)
64 xpss1 5653 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑥} ⊆ 𝐴 → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
6665adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
67 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (𝑓𝑦) ∈ ({𝑥} × 𝐴))
6866, 67sseldd 3946 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (𝑓𝑦) ∈ (𝐴 × 𝐴))
6968fvresd 6863 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = (1st ‘(𝑓𝑦)))
70 xp1st 7954 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → (1st ‘(𝑓𝑦)) ∈ {𝑥})
7167, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (1st ‘(𝑓𝑦)) ∈ {𝑥})
7269, 71eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) ∈ {𝑥})
73 elsni 4604 . . . . . . . . . . . . . . . . . . . . . 22 (((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) ∈ {𝑥} → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = 𝑥)
7472, 73syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = 𝑥)
7560, 74eqtrd 2773 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = 𝑥)
7617ffnd 6670 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵𝐶))
7776ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵𝐶))
7828a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝐵 ⊆ (𝐵𝐶))
79 fnfvima 7184 . . . . . . . . . . . . . . . . . . . . 21 ((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵𝐶) ∧ 𝐵 ⊆ (𝐵𝐶) ∧ 𝑦𝐵) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
8077, 78, 57, 79syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
8175, 80eqeltrrd 2835 . . . . . . . . . . . . . . . . . . 19 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
8281expr 458 . . . . . . . . . . . . . . . . . 18 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → (𝑦𝐵𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
8355, 82mtod 197 . . . . . . . . . . . . . . . . 17 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑦𝐵)
8483ex 414 . . . . . . . . . . . . . . . 16 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → ¬ 𝑦𝐵))
8584imim1d 82 . . . . . . . . . . . . . . 15 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((¬ 𝑦𝐵𝑦𝐶) → ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → 𝑦𝐶)))
8653, 85biimtrid 241 . . . . . . . . . . . . . 14 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝐵𝐶) → ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → 𝑦𝐶)))
8786impd 412 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → 𝑦𝐶))
8850, 87sylbid 239 . . . . . . . . . . . 12 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) → 𝑦𝐶))
8988ssrdv 3951 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶)
90 ssdomg 8943 . . . . . . . . . . 11 (𝐶 ∈ V → ((𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶 → (𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶))
9146, 89, 90sylc 65 . . . . . . . . . 10 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶)
92 f1ocnv 6797 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵𝐶))
93 f1of1 6784 . . . . . . . . . . . . . . 15 (𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵𝐶) → 𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶))
9492, 93syl 17 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶))
9594adantr 482 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶))
9631adantr 482 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐵𝐶) ∈ V)
97 vsnex 5387 . . . . . . . . . . . . . 14 {𝑥} ∈ V
9812adantr 482 . . . . . . . . . . . . . 14 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴 ∈ V)
99 xpexg 7685 . . . . . . . . . . . . . 14 (({𝑥} ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ∈ V)
10097, 98, 99sylancr 588 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ∈ V)
101 f1imaen2g 8958 . . . . . . . . . . . . 13 (((𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶) ∧ (𝐵𝐶) ∈ V) ∧ (({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴) ∧ ({𝑥} × 𝐴) ∈ V)) → (𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
10295, 96, 65, 100, 101syl22anc 838 . . . . . . . . . . . 12 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
103 vex 3448 . . . . . . . . . . . . 13 𝑥 ∈ V
104 xpsnen2g 9012 . . . . . . . . . . . . 13 ((𝑥 ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ≈ 𝐴)
105103, 98, 104sylancr 588 . . . . . . . . . . . 12 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ≈ 𝐴)
106 entr 8949 . . . . . . . . . . . 12 (((𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴) ∧ ({𝑥} × 𝐴) ≈ 𝐴) → (𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
107102, 105, 106syl2anc 585 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
108 domen1 9066 . . . . . . . . . . 11 ((𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴 → ((𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶𝐴𝐶))
109107, 108syl 17 . . . . . . . . . 10 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶𝐴𝐶))
11091, 109mpbid 231 . . . . . . . . 9 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴𝐶)
111110olcd 873 . . . . . . . 8 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐴* 𝐵𝐴𝐶))
112111ex 414 . . . . . . 7 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴* 𝐵𝐴𝐶)))
113112exlimdv 1937 . . . . . 6 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴* 𝐵𝐴𝐶)))
11442, 113biimtrid 241 . . . . 5 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ → (𝐴* 𝐵𝐴𝐶)))
11541, 114pm2.61dne 3028 . . . 4 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴* 𝐵𝐴𝐶))
116115exlimiv 1934 . . 3 (∃𝑓 𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴* 𝐵𝐴𝐶))
1172, 116sylbi 216 . 2 ((𝐵𝐶) ≈ (𝐴 × 𝐴) → (𝐴* 𝐵𝐴𝐶))
1181, 117syl 17 1 ((𝐴 × 𝐴) ≈ (𝐵𝐶) → (𝐴* 𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846   = wceq 1542  wex 1782  wcel 2107  wne 2940  Vcvv 3444  cdif 3908  cun 3909  wss 3911  c0 4283  {csn 4587   class class class wbr 5106   × cxp 5632  ccnv 5633  dom cdm 5634  ran crn 5635  cres 5636  cima 5637  ccom 5638  Fun wfun 6491   Fn wfn 6492  wf 6493  1-1wf1 6494  ontowfo 6495  1-1-ontowf1o 6496  cfv 6497  1st c1st 7920  cen 8883  cdom 8884  * cwdom 9505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-1st 7922  df-2nd 7923  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-wdom 9506
This theorem is referenced by:  unxpwdom  9530  ttac  41403
  Copyright terms: Public domain W3C validator