Theorem unxpwdom2 8762

Description: Lemma for unxpwdom 8763. (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.

Step	Hyp	Ref	Expression
1		ensym 8271	. 2 ⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐵 ∪ 𝐶) ≈ (𝐴 × 𝐴))
2		bren 8231	. . 3 ⊢ ((𝐵 ∪ 𝐶) ≈ (𝐴 × 𝐴) ↔ ∃𝑓 𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴))
3		ssdif0 4171	. . . . . 6 ⊢ (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ↔ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅)
4		dmxpid 5577	. . . . . . . . . . . . . 14 ⊢ dom (𝐴 × 𝐴) = 𝐴
5		f1ofo 6385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵 ∪ 𝐶)–onto→(𝐴 × 𝐴))
6		forn 6356	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(𝐵 ∪ 𝐶)–onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
7	5, 6	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
8		vex 3417	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
9	8	rnex 7362	. . . . . . . . . . . . . . . 16 ⊢ ran 𝑓 ∈ V
10	7, 9	syl6eqelr 2915	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 × 𝐴) ∈ V)
11	10	dmexd 7360	. . . . . . . . . . . . . 14 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → dom (𝐴 × 𝐴) ∈ V)
12	4, 11	syl5eqelr 2911	. . . . . . . . . . . . 13 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐴 ∈ V)
13		imassrn 5718	. . . . . . . . . . . . . 14 ⊢ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ ran ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)
14		f1stres 7452	. . . . . . . . . . . . . . . 16 ⊢ (1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴
15		f1of 6378	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴))
16		fco 6295	. . . . . . . . . . . . . . . 16 ⊢ (((1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴 ∧ 𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵 ∪ 𝐶)⟶𝐴)
17	14, 15, 16	sylancr 583	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵 ∪ 𝐶)⟶𝐴)
18	17	frnd 6285	. . . . . . . . . . . . . 14 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ran ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ⊆ 𝐴)
19	13, 18	syl5ss 3838	. . . . . . . . . . . . 13 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ 𝐴)
20	12, 19	ssexd 5030	. . . . . . . . . . . 12 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
21	20	adantr 474	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
22		simpr 479	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
23		ssdomg 8268	. . . . . . . . . . 11 ⊢ ((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
24	21, 22, 23	sylc 65	. . . . . . . . . 10 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
25		domwdom 8748	. . . . . . . . . 10 ⊢ (𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴 ≼* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
26	24, 25	syl 17	. . . . . . . . 9 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
27	17	ffund 6282	. . . . . . . . . . 11 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → Fun ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓))
28		ssun1 4003	. . . . . . . . . . . 12 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝐶)
29		f1odm 6382	. . . . . . . . . . . . 13 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → dom 𝑓 = (𝐵 ∪ 𝐶))
30	8	dmex 7361	. . . . . . . . . . . . 13 ⊢ dom 𝑓 ∈ V
31	29, 30	syl6eqelr 2915	. . . . . . . . . . . 12 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐵 ∪ 𝐶) ∈ V)
32		ssexg 5029	. . . . . . . . . . . 12 ⊢ ((𝐵 ⊆ (𝐵 ∪ 𝐶) ∧ (𝐵 ∪ 𝐶) ∈ V) → 𝐵 ∈ V)
33	28, 31, 32	sylancr 583	. . . . . . . . . . 11 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐵 ∈ V)
34		wdomima2g 8760	. . . . . . . . . . 11 ⊢ ((Fun ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ∧ 𝐵 ∈ V ∧ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
35	27, 33, 20, 34	syl3anc 1496	. . . . . . . . . 10 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
36	35	adantr 474	. . . . . . . . 9 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵)
37		wdomtr 8749	. . . . . . . . 9 ⊢ ((𝐴 ≼* (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∧ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵) → 𝐴 ≼* 𝐵)
38	26, 36, 37	syl2anc 581	. . . . . . . 8 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼* 𝐵)
39	38	orcd 906	. . . . . . 7 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
40	39	ex 403	. . . . . 6 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)))
41	3, 40	syl5bir 235	. . . . 5 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅ → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)))
42		n0 4160	. . . . . 6 ⊢ ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
43		ssun2 4004	. . . . . . . . . . . . 13 ⊢ 𝐶 ⊆ (𝐵 ∪ 𝐶)
44		ssexg 5029	. . . . . . . . . . . . 13 ⊢ ((𝐶 ⊆ (𝐵 ∪ 𝐶) ∧ (𝐵 ∪ 𝐶) ∈ V) → 𝐶 ∈ V)
45	43, 31, 44	sylancr 583	. . . . . . . . . . . 12 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐶 ∈ V)
46	45	adantr 474	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐶 ∈ V)
47		f1ofn 6379	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓 Fn (𝐵 ∪ 𝐶))
48		elpreima 6586	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn (𝐵 ∪ 𝐶) → (𝑦 ∈ (◡𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴))))
49	47, 48	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑦 ∈ (◡𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴))))
50	49	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (◡𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴))))
51		elun 3980	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (𝐵 ∪ 𝐶) ↔ (𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶))
52		df-or 881	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶) ↔ (¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
53	51, 52	bitri 267	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐵 ∪ 𝐶) ↔ (¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
54		eldifn 3960	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
55	54	ad2antlr 720	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
56	15	ad2antrr 719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴))
57		simprr 791	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
58	28, 57	sseldi 3825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (𝐵 ∪ 𝐶))
59		fvco3 6522	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴) ∧ 𝑦 ∈ (𝐵 ∪ 𝐶)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)))
60	56, 58, 59	syl2anc 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)))
61		eldifi 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝑥 ∈ 𝐴)
62	61	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝑥 ∈ 𝐴)
63	62	snssd 4558	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → {𝑥} ⊆ 𝐴)
64		xpss1 5361	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({𝑥} ⊆ 𝐴 → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
66	65	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
67		simprl 789	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (𝑓‘𝑦) ∈ ({𝑥} × 𝐴))
68	66, 67	sseldd 3828	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (𝑓‘𝑦) ∈ (𝐴 × 𝐴))
69		fvres 6452	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑦) ∈ (𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = (1st ‘(𝑓‘𝑦)))
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = (1st ‘(𝑓‘𝑦)))
71		xp1st 7460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → (1st ‘(𝑓‘𝑦)) ∈ {𝑥})
72	67, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (1st ‘(𝑓‘𝑦)) ∈ {𝑥})
73	70, 72	eqeltrd 2906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) ∈ {𝑥})
74		elsni 4414	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) ∈ {𝑥} → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = 𝑥)
75	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = 𝑥)
76	60, 75	eqtrd 2861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = 𝑥)
77	17	ffnd 6279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵 ∪ 𝐶))
78	77	ad2antrr 719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵 ∪ 𝐶))
79	28	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝐵 ⊆ (𝐵 ∪ 𝐶))
80		fnfvima 6752	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵 ∪ 𝐶) ∧ 𝐵 ⊆ (𝐵 ∪ 𝐶) ∧ 𝑦 ∈ 𝐵) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
81	78, 79, 57, 80	syl3anc 1496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
82	76, 81	eqeltrrd 2907	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
83	82	expr 450	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → (𝑦 ∈ 𝐵 → 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
84	55, 83	mtod 190	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑦 ∈ 𝐵)
85	84	ex 403	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → ¬ 𝑦 ∈ 𝐵))
86	85	imim1d 82	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → 𝑦 ∈ 𝐶)))
87	53, 86	syl5bi 234	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝐵 ∪ 𝐶) → ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → 𝑦 ∈ 𝐶)))
88	87	impd 400	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → 𝑦 ∈ 𝐶))
89	50, 88	sylbid 232	. . . . . . . . . . . 12 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (◡𝑓 “ ({𝑥} × 𝐴)) → 𝑦 ∈ 𝐶))
90	89	ssrdv 3833	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (◡𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶)
91		ssdomg 8268	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → ((◡𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶 → (◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶))
92	46, 90, 91	sylc 65	. . . . . . . . . 10 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶)
93		f1ocnv 6390	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ◡𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵 ∪ 𝐶))
94		f1of1 6377	. . . . . . . . . . . . . . 15 ⊢ (◡𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵 ∪ 𝐶) → ◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶))
95	93, 94	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶))
96	95	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶))
97	31	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐵 ∪ 𝐶) ∈ V)
98		snex 5129	. . . . . . . . . . . . . 14 ⊢ {𝑥} ∈ V
99	12	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴 ∈ V)
100		xpexg 7220	. . . . . . . . . . . . . 14 ⊢ (({𝑥} ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ∈ V)
101	98, 99, 100	sylancr 583	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ∈ V)
102		f1imaen2g 8283	. . . . . . . . . . . . 13 ⊢ (((◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶) ∧ (𝐵 ∪ 𝐶) ∈ V) ∧ (({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴) ∧ ({𝑥} × 𝐴) ∈ V)) → (◡𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
103	96, 97, 65, 101, 102	syl22anc 874	. . . . . . . . . . . 12 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (◡𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
104		vex 3417	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
105		xpsnen2g 8322	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ≈ 𝐴)
106	104, 99, 105	sylancr 583	. . . . . . . . . . . 12 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ≈ 𝐴)
107		entr 8274	. . . . . . . . . . . 12 ⊢ (((◡𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴) ∧ ({𝑥} × 𝐴) ≈ 𝐴) → (◡𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
108	103, 106, 107	syl2anc 581	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (◡𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
109		domen1 8371	. . . . . . . . . . 11 ⊢ ((◡𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴 → ((◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶 ↔ 𝐴 ≼ 𝐶))
110	108, 109	syl 17	. . . . . . . . . 10 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶 ↔ 𝐴 ≼ 𝐶))
111	92, 110	mpbid 224	. . . . . . . . 9 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴 ≼ 𝐶)
112	111	olcd 907	. . . . . . . 8 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
113	112	ex 403	. . . . . . 7 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)))
114	113	exlimdv 2034	. . . . . 6 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)))
115	42, 114	syl5bi 234	. . . . 5 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)))
116	41, 115	pm2.61dne 3085	. . . 4 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
117	116	exlimiv 2031	. . 3 ⊢ (∃𝑓 𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
118	2, 117	sylbi 209	. 2 ⊢ ((𝐵 ∪ 𝐶) ≈ (𝐴 × 𝐴) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
119	1, 118	syl 17	1 ⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 880   = wceq 1658  ∃wex 1880   ∈ wcel 2166   ≠ wne 2999  Vcvv 3414   ∖ cdif 3795   ∪ cun 3796   ⊆ wss 3798  ∅c0 4144  {csn 4397   class class class wbr 4873   × cxp 5340  ^◡ccnv 5341  dom cdm 5342  ran crn 5343   ↾ cres 5344   “ cima 5345   ∘ ccom 5346  Fun wfun 6117   Fn wfn 6118  ⟶wf 6119  –1-1→wf1 6120  –onto→wfo 6121  –1-1-onto→wf1o 6122  ‘cfv 6123  1^st c1st 7426   ≈ cen 8219   ≼ cdom 8220   ≼^* cwdom 8731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-1st 7428  df-2nd 7429  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-wdom 8733

This theorem is referenced by:  unxpwdom  8763  ttac  38446