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

Theorem unxpwdom2 8700
Description: Lemma for unxpwdom 8701. (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 8209 . 2 ((𝐴 × 𝐴) ≈ (𝐵𝐶) → (𝐵𝐶) ≈ (𝐴 × 𝐴))
2 bren 8169 . . 3 ((𝐵𝐶) ≈ (𝐴 × 𝐴) ↔ ∃𝑓 𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴))
3 ssdif0 4106 . . . . . 6 (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ↔ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅)
4 dmxpid 5513 . . . . . . . . . . . . . 14 dom (𝐴 × 𝐴) = 𝐴
5 f1ofo 6327 . . . . . . . . . . . . . . . . 17 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵𝐶)–onto→(𝐴 × 𝐴))
6 forn 6301 . . . . . . . . . . . . . . . . 17 (𝑓:(𝐵𝐶)–onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
75, 6syl 17 . . . . . . . . . . . . . . . 16 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
8 vex 3353 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
98rnex 7298 . . . . . . . . . . . . . . . 16 ran 𝑓 ∈ V
107, 9syl6eqelr 2853 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 × 𝐴) ∈ V)
11 dmexg 7295 . . . . . . . . . . . . . . 15 ((𝐴 × 𝐴) ∈ V → dom (𝐴 × 𝐴) ∈ V)
1210, 11syl 17 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → dom (𝐴 × 𝐴) ∈ V)
134, 12syl5eqelr 2849 . . . . . . . . . . . . 13 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐴 ∈ V)
14 imassrn 5659 . . . . . . . . . . . . . 14 (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ ran ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)
15 f1stres 7390 . . . . . . . . . . . . . . . 16 (1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴
16 f1of 6320 . . . . . . . . . . . . . . . 16 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴))
17 fco 6240 . . . . . . . . . . . . . . . 16 (((1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵𝐶)⟶𝐴)
1815, 16, 17sylancr 581 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵𝐶)⟶𝐴)
1918frnd 6230 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ran ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ⊆ 𝐴)
2014, 19syl5ss 3772 . . . . . . . . . . . . 13 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ 𝐴)
2113, 20ssexd 4966 . . . . . . . . . . . 12 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
2221adantr 472 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
23 simpr 477 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
24 ssdomg 8206 . . . . . . . . . . 11 ((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
2522, 23, 24sylc 65 . . . . . . . . . 10 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
26 domwdom 8686 . . . . . . . . . 10 (𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
2725, 26syl 17 . . . . . . . . 9 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
2818ffund 6227 . . . . . . . . . . 11 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → Fun ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓))
29 ssun1 3938 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵𝐶)
30 f1odm 6324 . . . . . . . . . . . . 13 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → dom 𝑓 = (𝐵𝐶))
318dmex 7297 . . . . . . . . . . . . 13 dom 𝑓 ∈ V
3230, 31syl6eqelr 2853 . . . . . . . . . . . 12 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐵𝐶) ∈ V)
33 ssexg 4965 . . . . . . . . . . . 12 ((𝐵 ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ∈ V) → 𝐵 ∈ V)
3429, 32, 33sylancr 581 . . . . . . . . . . 11 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐵 ∈ V)
35 wdomima2g 8698 . . . . . . . . . . 11 ((Fun ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ∧ 𝐵 ∈ V ∧ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
3628, 34, 21, 35syl3anc 1490 . . . . . . . . . 10 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
3736adantr 472 . . . . . . . . 9 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
38 wdomtr 8687 . . . . . . . . 9 ((𝐴* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∧ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵) → 𝐴* 𝐵)
3927, 37, 38syl2anc 579 . . . . . . . 8 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴* 𝐵)
4039orcd 899 . . . . . . 7 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴* 𝐵𝐴𝐶))
4140ex 401 . . . . . 6 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → (𝐴* 𝐵𝐴𝐶)))
423, 41syl5bir 234 . . . . 5 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅ → (𝐴* 𝐵𝐴𝐶)))
43 n0 4095 . . . . . 6 ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
44 ssun2 3939 . . . . . . . . . . . . 13 𝐶 ⊆ (𝐵𝐶)
45 ssexg 4965 . . . . . . . . . . . . 13 ((𝐶 ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ∈ V) → 𝐶 ∈ V)
4644, 32, 45sylancr 581 . . . . . . . . . . . 12 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐶 ∈ V)
4746adantr 472 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐶 ∈ V)
48 f1ofn 6321 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓 Fn (𝐵𝐶))
49 elpreima 6527 . . . . . . . . . . . . . . 15 (𝑓 Fn (𝐵𝐶) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴))))
5048, 49syl 17 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴))))
5150adantr 472 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴))))
52 elun 3915 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝐵𝐶) ↔ (𝑦𝐵𝑦𝐶))
53 df-or 874 . . . . . . . . . . . . . . . 16 ((𝑦𝐵𝑦𝐶) ↔ (¬ 𝑦𝐵𝑦𝐶))
5452, 53bitri 266 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐵𝐶) ↔ (¬ 𝑦𝐵𝑦𝐶))
55 eldifn 3895 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
5655ad2antlr 718 . . . . . . . . . . . . . . . . . 18 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
5716ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴))
58 simprr 789 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑦𝐵)
5929, 58sseldi 3759 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑦 ∈ (𝐵𝐶))
60 fvco3 6464 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓:(𝐵𝐶)⟶(𝐴 × 𝐴) ∧ 𝑦 ∈ (𝐵𝐶)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)))
6157, 59, 60syl2anc 579 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)))
62 eldifi 3894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝑥𝐴)
6362adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝑥𝐴)
6463snssd 4494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → {𝑥} ⊆ 𝐴)
65 xpss1 5296 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑥} ⊆ 𝐴 → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
6664, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
6766adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
68 simprl 787 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (𝑓𝑦) ∈ ({𝑥} × 𝐴))
6967, 68sseldd 3762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (𝑓𝑦) ∈ (𝐴 × 𝐴))
70 fvres 6394 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑦) ∈ (𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = (1st ‘(𝑓𝑦)))
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = (1st ‘(𝑓𝑦)))
72 xp1st 7398 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → (1st ‘(𝑓𝑦)) ∈ {𝑥})
7368, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (1st ‘(𝑓𝑦)) ∈ {𝑥})
7471, 73eqeltrd 2844 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) ∈ {𝑥})
75 elsni 4351 . . . . . . . . . . . . . . . . . . . . . 22 (((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) ∈ {𝑥} → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = 𝑥)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓𝑦)) = 𝑥)
7761, 76eqtrd 2799 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = 𝑥)
7818ffnd 6224 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵𝐶))
7978ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵𝐶))
8029a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝐵 ⊆ (𝐵𝐶))
81 fnfvima 6689 . . . . . . . . . . . . . . . . . . . . 21 ((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵𝐶) ∧ 𝐵 ⊆ (𝐵𝐶) ∧ 𝑦𝐵) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
8279, 80, 58, 81syl3anc 1490 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
8377, 82eqeltrrd 2845 . . . . . . . . . . . . . . . . . . 19 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦𝐵)) → 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
8483expr 448 . . . . . . . . . . . . . . . . . 18 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → (𝑦𝐵𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
8556, 84mtod 189 . . . . . . . . . . . . . . . . 17 (((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑦𝐵)
8685ex 401 . . . . . . . . . . . . . . . 16 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → ¬ 𝑦𝐵))
8786imim1d 82 . . . . . . . . . . . . . . 15 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((¬ 𝑦𝐵𝑦𝐶) → ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → 𝑦𝐶)))
8854, 87syl5bi 233 . . . . . . . . . . . . . 14 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝐵𝐶) → ((𝑓𝑦) ∈ ({𝑥} × 𝐴) → 𝑦𝐶)))
8988impd 398 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑦 ∈ (𝐵𝐶) ∧ (𝑓𝑦) ∈ ({𝑥} × 𝐴)) → 𝑦𝐶))
9051, 89sylbid 231 . . . . . . . . . . . 12 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝑓 “ ({𝑥} × 𝐴)) → 𝑦𝐶))
9190ssrdv 3767 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶)
92 ssdomg 8206 . . . . . . . . . . 11 (𝐶 ∈ V → ((𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶 → (𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶))
9347, 91, 92sylc 65 . . . . . . . . . 10 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶)
94 f1ocnv 6332 . . . . . . . . . . . . . . 15 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵𝐶))
95 f1of1 6319 . . . . . . . . . . . . . . 15 (𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵𝐶) → 𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶))
9694, 95syl 17 . . . . . . . . . . . . . 14 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶))
9796adantr 472 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶))
9832adantr 472 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐵𝐶) ∈ V)
99 snex 5064 . . . . . . . . . . . . . 14 {𝑥} ∈ V
10013adantr 472 . . . . . . . . . . . . . 14 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴 ∈ V)
101 xpexg 7158 . . . . . . . . . . . . . 14 (({𝑥} ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ∈ V)
10299, 100, 101sylancr 581 . . . . . . . . . . . . 13 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ∈ V)
103 f1imaen2g 8221 . . . . . . . . . . . . 13 (((𝑓:(𝐴 × 𝐴)–1-1→(𝐵𝐶) ∧ (𝐵𝐶) ∈ V) ∧ (({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴) ∧ ({𝑥} × 𝐴) ∈ V)) → (𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
10497, 98, 66, 102, 103syl22anc 867 . . . . . . . . . . . 12 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
105 vex 3353 . . . . . . . . . . . . 13 𝑥 ∈ V
106 xpsnen2g 8260 . . . . . . . . . . . . 13 ((𝑥 ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ≈ 𝐴)
107105, 100, 106sylancr 581 . . . . . . . . . . . 12 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ≈ 𝐴)
108 entr 8212 . . . . . . . . . . . 12 (((𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴) ∧ ({𝑥} × 𝐴) ≈ 𝐴) → (𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
109104, 107, 108syl2anc 579 . . . . . . . . . . 11 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
110 domen1 8309 . . . . . . . . . . 11 ((𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴 → ((𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶𝐴𝐶))
111109, 110syl 17 . . . . . . . . . 10 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶𝐴𝐶))
11293, 111mpbid 223 . . . . . . . . 9 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴𝐶)
113112olcd 900 . . . . . . . 8 ((𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐴* 𝐵𝐴𝐶))
114113ex 401 . . . . . . 7 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴* 𝐵𝐴𝐶)))
115114exlimdv 2028 . . . . . 6 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴* 𝐵𝐴𝐶)))
11643, 115syl5bi 233 . . . . 5 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ → (𝐴* 𝐵𝐴𝐶)))
11742, 116pm2.61dne 3023 . . . 4 (𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴* 𝐵𝐴𝐶))
118117exlimiv 2025 . . 3 (∃𝑓 𝑓:(𝐵𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴* 𝐵𝐴𝐶))
1192, 118sylbi 208 . 2 ((𝐵𝐶) ≈ (𝐴 × 𝐴) → (𝐴* 𝐵𝐴𝐶))
1201, 119syl 17 1 ((𝐴 × 𝐴) ≈ (𝐵𝐶) → (𝐴* 𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873   = wceq 1652  wex 1874  wcel 2155  wne 2937  Vcvv 3350  cdif 3729  cun 3730  wss 3732  c0 4079  {csn 4334   class class class wbr 4809   × cxp 5275  ccnv 5276  dom cdm 5277  ran crn 5278  cres 5279  cima 5280  ccom 5281  Fun wfun 6062   Fn wfn 6063  wf 6064  1-1wf1 6065  ontowfo 6066  1-1-ontowf1o 6067  cfv 6068  1st c1st 7364  cen 8157  cdom 8158  * cwdom 8669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-1st 7366  df-2nd 7367  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-wdom 8671
This theorem is referenced by:  unxpwdom  8701  ttac  38280
  Copyright terms: Public domain W3C validator