unxpwdom2 - Metamath Proof Explorer

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

Theorem unxpwdom2 9474

Description: Lemma for unxpwdom 9475. (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 8925	. 2 ⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐵 ∪ 𝐶) ≈ (𝐴 × 𝐴))
2		bren 8879	. . 3 ⊢ ((𝐵 ∪ 𝐶) ≈ (𝐴 × 𝐴) ↔ ∃𝑓 𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴))
3		ssdif0 4313	. . . . . 6 ⊢ (𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ↔ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅)
4		dmxpid 5869	. . . . . . . . . . . . . 14 ⊢ dom (𝐴 × 𝐴) = 𝐴
5		f1ofo 6770	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵 ∪ 𝐶)–onto→(𝐴 × 𝐴))
6		forn 6738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(𝐵 ∪ 𝐶)–onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
7	5, 6	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴))
8		vex 3440	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
9	8	rnex 7840	. . . . . . . . . . . . . . . 16 ⊢ ran 𝑓 ∈ V
10	7, 9	eqeltrrdi 2840	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 × 𝐴) ∈ V)
11	10	dmexd 7833	. . . . . . . . . . . . . 14 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → dom (𝐴 × 𝐴) ∈ V)
12	4, 11	eqeltrrid 2836	. . . . . . . . . . . . 13 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐴 ∈ V)
13		imassrn 6019	. . . . . . . . . . . . . 14 ⊢ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ ran ((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓)
14		f1stres 7945	. . . . . . . . . . . . . . . 16 ⊢ (1^st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴
15		f1of 6763	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴))
16		fco 6675	. . . . . . . . . . . . . . . 16 ⊢ (((1^st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴 ∧ 𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴)) → ((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵 ∪ 𝐶)⟶𝐴)
17	14, 15, 16	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵 ∪ 𝐶)⟶𝐴)
18	17	frnd 6659	. . . . . . . . . . . . . 14 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ran ((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ⊆ 𝐴)
19	13, 18	sstrid 3941	. . . . . . . . . . . . 13 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ 𝐴)
20	12, 19	ssexd 5260	. . . . . . . . . . . 12 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
21	20	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V)
22		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
23		ssdomg 8922	. . . . . . . . . . 11 ⊢ ((((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V → (𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴 ≼ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
24	21, 22, 23	sylc 65	. . . . . . . . . 10 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
25		domwdom 9460	. . . . . . . . . 10 ⊢ (𝐴 ≼ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴 ≼^* (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
26	24, 25	syl 17	. . . . . . . . 9 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼^* (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
27	17	ffund 6655	. . . . . . . . . . 11 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → Fun ((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓))
28		ssun1 4125	. . . . . . . . . . . 12 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝐶)
29		f1odm 6767	. . . . . . . . . . . . 13 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → dom 𝑓 = (𝐵 ∪ 𝐶))
30	8	dmex 7839	. . . . . . . . . . . . 13 ⊢ dom 𝑓 ∈ V
31	29, 30	eqeltrrdi 2840	. . . . . . . . . . . 12 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐵 ∪ 𝐶) ∈ V)
32		ssexg 5259	. . . . . . . . . . . 12 ⊢ ((𝐵 ⊆ (𝐵 ∪ 𝐶) ∧ (𝐵 ∪ 𝐶) ∈ V) → 𝐵 ∈ V)
33	28, 31, 32	sylancr 587	. . . . . . . . . . 11 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐵 ∈ V)
34		wdomima2g 9472	. . . . . . . . . . 11 ⊢ ((Fun ((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ∧ 𝐵 ∈ V ∧ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼^* 𝐵)
35	27, 33, 20, 34	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼^* 𝐵)
36	35	adantr 480	. . . . . . . . 9 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼^* 𝐵)
37		wdomtr 9461	. . . . . . . . 9 ⊢ ((𝐴 ≼^* (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∧ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼^* 𝐵) → 𝐴 ≼^* 𝐵)
38	26, 36, 37	syl2anc 584	. . . . . . . 8 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼^* 𝐵)
39	38	orcd 873	. . . . . . 7 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶))
40	39	ex 412	. . . . . 6 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ⊆ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶)))
41	3, 40	biimtrrid 243	. . . . 5 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅ → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶)))
42		n0 4300	. . . . . 6 ⊢ ((𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
43		ssun2 4126	. . . . . . . . . . . . 13 ⊢ 𝐶 ⊆ (𝐵 ∪ 𝐶)
44		ssexg 5259	. . . . . . . . . . . . 13 ⊢ ((𝐶 ⊆ (𝐵 ∪ 𝐶) ∧ (𝐵 ∪ 𝐶) ∈ V) → 𝐶 ∈ V)
45	43, 31, 44	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐶 ∈ V)
46	45	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐶 ∈ V)
47		f1ofn 6764	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓 Fn (𝐵 ∪ 𝐶))
48		elpreima 6991	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn (𝐵 ∪ 𝐶) → (𝑦 ∈ (^◡𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴))))
49	47, 48	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑦 ∈ (^◡𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴))))
50	49	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (^◡𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴))))
51		elun 4100	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (𝐵 ∪ 𝐶) ↔ (𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶))
52		df-or 848	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶) ↔ (¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
53	51, 52	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐵 ∪ 𝐶) ↔ (¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
54		eldifn 4079	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → ¬ 𝑥 ∈ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
55	54	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑥 ∈ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
56	15	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴))
57		simprr 772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
58	28, 57	sselid 3927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (𝐵 ∪ 𝐶))
59		fvco3 6921	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴) ∧ 𝑦 ∈ (𝐵 ∪ 𝐶)) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1^st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)))
60	56, 58, 59	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1^st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)))
61		eldifi 4078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝑥 ∈ 𝐴)
62	61	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝑥 ∈ 𝐴)
63	62	snssd 4758	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → {𝑥} ⊆ 𝐴)
64		xpss1 5633	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({𝑥} ⊆ 𝐴 → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
66	65	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴))
67		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (𝑓‘𝑦) ∈ ({𝑥} × 𝐴))
68	66, 67	sseldd 3930	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (𝑓‘𝑦) ∈ (𝐴 × 𝐴))
69	68	fvresd 6842	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1^st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = (1^st ‘(𝑓‘𝑦)))
70		xp1st 7953	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → (1^st ‘(𝑓‘𝑦)) ∈ {𝑥})
71	67, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (1^st ‘(𝑓‘𝑦)) ∈ {𝑥})
72	69, 71	eqeltrd 2831	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1^st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) ∈ {𝑥})
73		elsni 4590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) ∈ {𝑥} → ((1^st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = 𝑥)
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1^st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = 𝑥)
75	60, 74	eqtrd 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = 𝑥)
76	17	ffnd 6652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵 ∪ 𝐶))
77	76	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵 ∪ 𝐶))
78	28	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝐵 ⊆ (𝐵 ∪ 𝐶))
79		fnfvima 7167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵 ∪ 𝐶) ∧ 𝐵 ⊆ (𝐵 ∪ 𝐶) ∧ 𝑦 ∈ 𝐵) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
80	77, 78, 57, 79	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
81	75, 80	eqeltrrd 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))
82	81	expr 456	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → (𝑦 ∈ 𝐵 → 𝑥 ∈ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)))
83	55, 82	mtod 198	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑦 ∈ 𝐵)
84	83	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → ¬ 𝑦 ∈ 𝐵))
85	84	imim1d 82	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → 𝑦 ∈ 𝐶)))
86	53, 85	biimtrid 242	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝐵 ∪ 𝐶) → ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → 𝑦 ∈ 𝐶)))
87	86	impd 410	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → 𝑦 ∈ 𝐶))
88	50, 87	sylbid 240	. . . . . . . . . . . 12 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (^◡𝑓 “ ({𝑥} × 𝐴)) → 𝑦 ∈ 𝐶))
89	88	ssrdv 3935	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (^◡𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶)
90		ssdomg 8922	. . . . . . . . . . 11 ⊢ (𝐶 ∈ V → ((^◡𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶 → (^◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶))
91	46, 89, 90	sylc 65	. . . . . . . . . 10 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (^◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶)
92		f1ocnv 6775	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ^◡𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵 ∪ 𝐶))
93		f1of1 6762	. . . . . . . . . . . . . . 15 ⊢ (^◡𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵 ∪ 𝐶) → ^◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶))
94	92, 93	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ^◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶))
95	94	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ^◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶))
96	31	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐵 ∪ 𝐶) ∈ V)
97		vsnex 5370	. . . . . . . . . . . . . 14 ⊢ {𝑥} ∈ V
98	12	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴 ∈ V)
99		xpexg 7683	. . . . . . . . . . . . . 14 ⊢ (({𝑥} ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ∈ V)
100	97, 98, 99	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ∈ V)
101		f1imaen2g 8937	. . . . . . . . . . . . 13 ⊢ (((^◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶) ∧ (𝐵 ∪ 𝐶) ∈ V) ∧ (({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴) ∧ ({𝑥} × 𝐴) ∈ V)) → (^◡𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
102	95, 96, 65, 100, 101	syl22anc 838	. . . . . . . . . . . 12 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (^◡𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴))
103		vex 3440	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
104		xpsnen2g 8983	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ≈ 𝐴)
105	103, 98, 104	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ≈ 𝐴)
106		entr 8928	. . . . . . . . . . . 12 ⊢ (((^◡𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴) ∧ ({𝑥} × 𝐴) ≈ 𝐴) → (^◡𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
107	102, 105, 106	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (^◡𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴)
108		domen1 9032	. . . . . . . . . . 11 ⊢ ((^◡𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴 → ((^◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶 ↔ 𝐴 ≼ 𝐶))
109	107, 108	syl 17	. . . . . . . . . 10 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((^◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶 ↔ 𝐴 ≼ 𝐶))
110	91, 109	mpbid 232	. . . . . . . . 9 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴 ≼ 𝐶)
111	110	olcd 874	. . . . . . . 8 ⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶))
112	111	ex 412	. . . . . . 7 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶)))
113	112	exlimdv 1934	. . . . . 6 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (∃𝑥 𝑥 ∈ (𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶)))
114	42, 113	biimtrid 242	. . . . 5 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1^st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶)))
115	41, 114	pm2.61dne 3014	. . . 4 ⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶))
116	115	exlimiv 1931	. . 3 ⊢ (∃𝑓 𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶))
117	2, 116	sylbi 217	. 2 ⊢ ((𝐵 ∪ 𝐶) ≈ (𝐴 × 𝐴) → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶))
118	1, 117	syl 17	1 ⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐴 ≼^* 𝐵 ∨ 𝐴 ≼ 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ≠ wne 2928 Vcvv 3436 ∖ cdif 3894 ∪ cun 3895 ⊆ wss 3897 ∅c0 4280 {csn 4573 class class class wbr 5089 × cxp 5612 ^◡ccnv 5613 dom cdm 5614 ran crn 5615 ↾ cres 5616 “ cima 5617 ∘ ccom 5618 Fun wfun 6475 Fn wfn 6476 ⟶wf 6477 –1-1→wf1 6478 –onto→wfo 6479 –1-1-onto→wf1o 6480 ‘cfv 6481 1^st c1st 7919 ≈ cen 8866 ≼ cdom 8867 ≼^* cwdom 9450

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-1st 7921 df-2nd 7922 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-wdom 9451

This theorem is referenced by: unxpwdom 9475 ttac 43139

W3C validator