Theorem infxpidmlem12 4944

Description: Lemma for infxpidm 4945. Letting x be the range of a maximal bijection g in H, infxpidmlem11 4943 lets us show that assuming x ≼ (A ∖ x) leads to the contradiction ∃h ∈ Hg ⊂ h meaning g is not maximal. Thus (A ∖ x) ≺ x. This allows us to show that x is as big as A. Since x is idempotent, and g exists by Zorn's Lemma in infxpidmlem9 4941, A is also idempotent.

Hypotheses

Ref	Expression
infxpidmlem.1	⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))}
infxpidmlem.2	⊢ A ∈ V

Assertion

Ref	Expression
infxpidmlem12	⊢ (ω ≼ A → (A × A) ≈ A)

Distinct variable group(s):   t,f,A

Proof of Theorem infxpidmlem12

Step	Hyp	Ref	Expression
1		infxpidmlem.1	. . 3 ⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))}
2		infxpidmlem.2	. . 3 ⊢ A ∈ V
3	1, 2	infxpidmlem9 4941	. 2 ⊢ ∃g ∈ H ∀h ∈ H ¬ g ⊂ h
4	1, 2	infxpidmlem10 4942	. . . . 5 ⊢ (∀h ∈ H ¬ g ⊂ h → (ω ≼ A → ¬ g = ∅))
5		visset 1350	. . . . . . . . 9 ⊢ g ∈ V
6	1, 5	infxpidmlem2 4934	. . . . . . . 8 ⊢ (g ∈ H ↔ (g = ∅ ∨ ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x)))
7		df-or 197	. . . . . . . 8 ⊢ ((g = ∅ ∨ ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x)) ↔ (¬ g = ∅ → ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x)))
8	6, 7	bitr 151	. . . . . . 7 ⊢ (g ∈ H ↔ (¬ g = ∅ → ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x)))
9		entrt 3319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((x × y) ∪ ((y × x) ∪ (y × y))) ≈ x ∧ x ≈ y) → ((x × y) ∪ ((y × x) ∪ (y × y))) ≈ y)
10		entrt 3319	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((x ≈ (x × x) ∧ (x × x) ≈ (x × y)) → x ≈ (x × y))
11		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ x ∈ V
12	11	enref 3295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ x ≈ x
13		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ y ∈ V
14	11, 11, 11, 13	xpen 3383	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((x ≈ x ∧ x ≈ y) → (x × x) ≈ (x × y))
15	12, 14	mpan 518	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x ≈ y → (x × x) ≈ (x × y))
16	10, 15	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((x ≈ (x × x) ∧ x ≈ y) → x ≈ (x × y))
17	16	adantll 309	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ω ≼ x ∧ x ≈ (x × x)) ∧ x ≈ y) → x ≈ (x × y))
18		entrt 3319	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((x ≈ (x × x) ∧ (x × x) ≈ (y × x)) → x ≈ (y × x))
19	11, 13, 11, 11	xpen 3383	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((x ≈ y ∧ x ≈ x) → (x × x) ≈ (y × x))
20	12, 19	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (x ≈ y → (x × x) ≈ (y × x))
21	18, 20	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((x ≈ (x × x) ∧ x ≈ y) → x ≈ (y × x))
22		entrt 3319	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((x ≈ (x × x) ∧ (x × x) ≈ (y × y)) → x ≈ (y × y))
23	11, 13, 11, 13	xpen 3383	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((x ≈ y ∧ x ≈ y) → (x × x) ≈ (y × y))
24	23	anidms 332	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (x ≈ y → (x × x) ≈ (y × y))
25	22, 24	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((x ≈ (x × x) ∧ x ≈ y) → x ≈ (y × y))
26	21, 25	jca 236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((x ≈ (x × x) ∧ x ≈ y) → (x ≈ (y × x) ∧ x ≈ (y × y)))
27	26	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ω ≼ x ∧ x ≈ (x × x)) ∧ x ≈ y) → (x ≈ (y × x) ∧ x ≈ (y × y)))
28	13, 11	xpex 2488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (y × x) ∈ V
29	13, 13	xpex 2488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (y × y) ∈ V
30	28, 29	infxpidmlem1 4933	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ω ≼ x ∧ x ≈ (x × x)) → ((x ≈ (y × x) ∧ x ≈ (y × y)) → x ≈ ((y × x) ∪ (y × y))))
31	30	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ω ≼ x ∧ x ≈ (x × x)) ∧ x ≈ y) → ((x ≈ (y × x) ∧ x ≈ (y × y)) → x ≈ ((y × x) ∪ (y × y))))
32	27, 31	mpd 46	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ω ≼ x ∧ x ≈ (x × x)) ∧ x ≈ y) → x ≈ ((y × x) ∪ (y × y)))
33	11, 13	xpex 2488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x × y) ∈ V
34	28, 29	unex 1949	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((y × x) ∪ (y × y)) ∈ V
35	33, 34	infxpidmlem1 4933	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ≼ x ∧ x ≈ (x × x)) → ((x ≈ (x × y) ∧ x ≈ ((y × x) ∪ (y × y))) → x ≈ ((x × y) ∪ ((y × x) ∪ (y × y)))))
36	35	adantr 306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ω ≼ x ∧ x ≈ (x × x)) ∧ x ≈ y) → ((x ≈ (x × y) ∧ x ≈ ((y × x) ∪ (y × y))) → x ≈ ((x × y) ∪ ((y × x) ∪ (y × y)))))
37	17, 32, 36	mp2and 526	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ω ≼ x ∧ x ≈ (x × x)) ∧ x ≈ y) → x ≈ ((x × y) ∪ ((y × x) ∪ (y × y))))
38	33, 34	unex 1949	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((x × y) ∪ ((y × x) ∪ (y × y))) ∈ V
39	38	ensym 3317	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x ≈ ((x × y) ∪ ((y × x) ∪ (y × y))) → ((x × y) ∪ ((y × x) ∪ (y × y))) ≈ x)
40	37, 39	syl 12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ≼ x ∧ x ≈ (x × x)) ∧ x ≈ y) → ((x × y) ∪ ((y × x) ∪ (y × y))) ≈ x)
41		pm3.27 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ≼ x ∧ x ≈ (x × x)) ∧ x ≈ y) → x ≈ y)
42	9, 40, 41	sylanc 361	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ω ≼ x ∧ x ≈ (x × x)) ∧ x ≈ y) → ((x × y) ∪ ((y × x) ∪ (y × y))) ≈ y)
43	11	ensym 3317	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((x × x) ≈ x → x ≈ (x × x))
44	42, 43	sylan12 355	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ω ≼ x ∧ (x × x) ≈ x) ∧ x ≈ y) → ((x × y) ∪ ((y × x) ∪ (y × y))) ≈ y)
45	13	bren 3282	. . . . . . . . . . . . . . . . . . 19 ⊢ (((x × y) ∪ ((y × x) ∪ (y × y))) ≈ y ↔ ∃u u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)
46	44, 45	sylib 173	. . . . . . . . . . . . . . . . . 18 ⊢ (((ω ≼ x ∧ (x × x) ≈ x) ∧ x ≈ y) → ∃u u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)
47	11, 11	xpex 2488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x × x) ∈ V
48	47	f1oen 3301	. . . . . . . . . . . . . . . . . . . 20 ⊢ (g:(x × x)–1-1-onto→x → (x × x) ≈ x)
49	48	anim2i 270	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ≼ x ∧ g:(x × x)–1-1-onto→x) → (ω ≼ x ∧ (x × x) ≈ x))
50	49	adantlr 310	. . . . . . . . . . . . . . . . . 18 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (ω ≼ x ∧ (x × x) ≈ x))
51	46, 50	sylan 343	. . . . . . . . . . . . . . . . 17 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) ∧ x ≈ y) → ∃u u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)
52	51	adantrr 312	. . . . . . . . . . . . . . . 16 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) → ∃u u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)
53	1, 2	infxpidmlem11 4943	. . . . . . . . . . . . . . . . . 18 ⊢ (((((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → ∃h ∈ H g ⊂ h)
54	53	exp 291	. . . . . . . . . . . . . . . . 17 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) → (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → ∃h ∈ H g ⊂ h))
55	54	19.23adv 954	. . . . . . . . . . . . . . . 16 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) → (∃u u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → ∃h ∈ H g ⊂ h))
56	52, 55	mpd 46	. . . . . . . . . . . . . . 15 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) → ∃h ∈ H g ⊂ h)
57	56	exp 291	. . . . . . . . . . . . . 14 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → ((x ≈ y ∧ y ⊆ (A ∖ x)) → ∃h ∈ H g ⊂ h))
58	57	19.23adv 954	. . . . . . . . . . . . 13 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (∃y(x ≈ y ∧ y ⊆ (A ∖ x)) → ∃h ∈ H g ⊂ h))
59		difexg 1703	. . . . . . . . . . . . . . 15 ⊢ (A ∈ V → (A ∖ x) ∈ V)
60	2, 59	ax-mp 6	. . . . . . . . . . . . . 14 ⊢ (A ∖ x) ∈ V
61	60	domen 3284	. . . . . . . . . . . . 13 ⊢ (x ≼ (A ∖ x) ↔ ∃y(x ≈ y ∧ y ⊆ (A ∖ x)))
62	58, 61	syl5ib 181	. . . . . . . . . . . 12 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (x ≼ (A ∖ x) → ∃h ∈ H g ⊂ h))
63		domtri 3644	. . . . . . . . . . . . 13 ⊢ ((x ∈ V ∧ (A ∖ x) ∈ V) → (x ≼ (A ∖ x) ↔ ¬ (A ∖ x) ≺ x))
64	11, 60, 63	mp2an 520	. . . . . . . . . . . 12 ⊢ (x ≼ (A ∖ x) ↔ ¬ (A ∖ x) ≺ x)
65		dfrex2 1212	. . . . . . . . . . . 12 ⊢ (∃h ∈ H g ⊂ h ↔ ¬ ∀h ∈ H ¬ g ⊂ h)
66	62, 64, 65	3imtr3g 425	. . . . . . . . . . 11 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (¬ (A ∖ x) ≺ x → ¬ ∀h ∈ H ¬ g ⊂ h))
67	66	a3d 70	. . . . . . . . . 10 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (∀h ∈ H ¬ g ⊂ h → (A ∖ x) ≺ x))
68		sbth 3359	. . . . . . . . . . . . . . . 16 ⊢ ((A ≼ x ∧ x ≼ A) → A ≈ x)
69		domentr 3326	. . . . . . . . . . . . . . . . 17 ⊢ ((A ≼ (x × x) ∧ (x × x) ≈ x) → A ≼ x)
70	11, 60	unxpdom2 3651	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1o ≺ x ∧ (A ∖ x) ≼ x) → (x ∪ (A ∖ x)) ≼ (x × x))
71		ssun2 1622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ A ⊆ (x ∪ A)
72		ssdomg 3311	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (A ∈ V → (A ⊆ (x ∪ A) → A ≼ (x ∪ A)))
73	2, 71, 72	mp2 43	. . . . . . . . . . . . . . . . . . . . 21 ⊢ A ≼ (x ∪ A)
74		undif2 1762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x ∪ (A ∖ x)) = (x ∪ A)
75	73, 74	breqtrr 2082	. . . . . . . . . . . . . . . . . . . 20 ⊢ A ≼ (x ∪ (A ∖ x))
76		domtr 3320	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((A ≼ (x ∪ (A ∖ x)) ∧ (x ∪ (A ∖ x)) ≼ (x × x)) → A ≼ (x × x))
77	75, 76	mpan 518	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x ∪ (A ∖ x)) ≼ (x × x) → A ≼ (x × x))
78	70, 77	syl 12	. . . . . . . . . . . . . . . . . 18 ⊢ ((1o ≺ x ∧ (A ∖ x) ≼ x) → A ≼ (x × x))
79		1onn 3193	. . . . . . . . . . . . . . . . . . 19 ⊢ 1o ∈ ω
80	11	infsdomnn 3426	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ≼ x ∧ 1o ∈ ω) → 1o ≺ x)
81	79, 80	mpan2 519	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ x → 1o ≺ x)
82		sdomdom 3290	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ∖ x) ≺ x → (A ∖ x) ≼ x)
83	78, 81, 82	syl2an 349	. . . . . . . . . . . . . . . . 17 ⊢ ((ω ≼ x ∧ (A ∖ x) ≺ x) → A ≼ (x × x))
84	69, 83	sylan 343	. . . . . . . . . . . . . . . 16 ⊢ (((ω ≼ x ∧ (A ∖ x) ≺ x) ∧ (x × x) ≈ x) → A ≼ x)
85		ssdomg 3311	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ V → (x ⊆ A → x ≼ A))
86	11, 85	ax-mp 6	. . . . . . . . . . . . . . . 16 ⊢ (x ⊆ A → x ≼ A)
87	68, 84, 86	syl2an 349	. . . . . . . . . . . . . . 15 ⊢ ((((ω ≼ x ∧ (A ∖ x) ≺ x) ∧ (x × x) ≈ x) ∧ x ⊆ A) → A ≈ x)
88		entrt 3319	. . . . . . . . . . . . . . . . . . 19 ⊢ (((A × A) ≈ x ∧ x ≈ A) → (A × A) ≈ A)
89		entrt 3319	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((A × A) ≈ (x × x) ∧ (x × x) ≈ x) → (A × A) ≈ x)
90	2, 11, 2, 11	xpen 3383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((A ≈ x ∧ A ≈ x) → (A × A) ≈ (x × x))
91	90	anidms 332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (A ≈ x → (A × A) ≈ (x × x))
92	89, 91	sylan 343	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ≈ x ∧ (x × x) ≈ x) → (A × A) ≈ x)
93	11	ensym 3317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (A ≈ x → x ≈ A)
94	93	adantr 306	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ≈ x ∧ (x × x) ≈ x) → x ≈ A)
95	88, 92, 94	sylanc 361	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ≈ x ∧ (x × x) ≈ x) → (A × A) ≈ A)
96	95	ancoms 334	. . . . . . . . . . . . . . . . 17 ⊢ (((x × x) ≈ x ∧ A ≈ x) → (A × A) ≈ A)
97	96	exp 291	. . . . . . . . . . . . . . . 16 ⊢ ((x × x) ≈ x → (A ≈ x → (A × A) ≈ A))
98	97	ad2antlr 321	. . . . . . . . . . . . . . 15 ⊢ ((((ω ≼ x ∧ (A ∖ x) ≺ x) ∧ (x × x) ≈ x) ∧ x ⊆ A) → (A ≈ x → (A × A) ≈ A))
99	87, 98	mpd 46	. . . . . . . . . . . . . 14 ⊢ ((((ω ≼ x ∧ (A ∖ x) ≺ x) ∧ (x × x) ≈ x) ∧ x ⊆ A) → (A × A) ≈ A)
100	99	exp41 299	. . . . . . . . . . . . 13 ⊢ (ω ≼ x → ((A ∖ x) ≺ x → ((x × x) ≈ x → (x ⊆ A → (A × A) ≈ A))))
101	100	com24 37	. . . . . . . . . . . 12 ⊢ (ω ≼ x → (x ⊆ A → ((x × x) ≈ x → ((A ∖ x) ≺ x → (A × A) ≈ A))))
102	101	imp31 280	. . . . . . . . . . 11 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ (x × x) ≈ x) → ((A ∖ x) ≺ x → (A × A) ≈ A))
103	102, 48	sylan2 346	. . . . . . . . . 10 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → ((A ∖ x) ≺ x → (A × A) ≈ A))
104	67, 103	syld 27	. . . . . . . . 9 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (∀h ∈ H ¬ g ⊂ h → (A × A) ≈ A))
105	104	19.23aiv 952	. . . . . . . 8 ⊢ (∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (∀h ∈ H ¬ g ⊂ h → (A × A) ≈ A))
106	105	syl3 18	. . . . . . 7 ⊢ ((¬ g = ∅ → ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x)) → (¬ g = ∅ → (∀h ∈ H ¬ g ⊂ h → (A × A) ≈ A)))
107	8, 106	sylbi 174	. . . . . 6 ⊢ (g ∈ H → (¬ g = ∅ → (∀h ∈ H ¬ g ⊂ h → (A × A) ≈ A)))
108	107	com13 33	. . . . 5 ⊢ (∀h ∈ H ¬ g ⊂ h → (¬ g = ∅ → (g ∈ H → (A × A) ≈ A)))
109	4, 108	syld 27	. . . 4 ⊢ (∀h ∈ H ¬ g ⊂ h → (ω ≼ A → (g ∈ H → (A × A) ≈ A)))
110	109	com3r 35	. . 3 ⊢ (g ∈ H → (∀h ∈ H ¬ g ⊂ h → (ω ≼ A → (A × A) ≈ A)))
111	110	r19.23aiv 1284	. 2 ⊢ (∃g ∈ H ∀h ∈ H ¬ g ⊂ h → (ω ≼ A → (A × A) ≈ A))
112	3, 111	ax-mp 6	1 ⊢ (ω ≼ A → (A × A) ≈ A)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196  ∃wex 678  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  Vcvv 1348   ∖ cdif 1484   ∪ cun 1485   ⊆ wss 1487   ⊂ wpss 1488  ∅c0 1707   class class class wbr 2054  ωcom 2372   × cxp 2408  –1-1-onto→wf1o 2421  1_oc1o 3099   ≈ cen 3271   ≼ cdom 3272   ≺ csdm 3273

This theorem is referenced by:  infxpidm 4945

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079  ax-ac 1080

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-iso 2439  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1st 3087  df-2nd 3088  df-1o 3104  df-2o 3105  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-en 3274  df-dom 3275  df-sdom 3276  df-card 3623  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-plp 3882  df-mp 3883  df-ltp 3884  df-plpr 3958  df-mpr 3959  df-enr 3960  df-nr 3961  df-plr 3962  df-mr 3963  df-ltr 3964  df-0r 3965  df-1r 3966  df-m1r 3967  df-c 4034  df-0 4035  df-1 4036  df-r 4038  df-plus 4039  df-mul 4040  df-lt 4041  df-sub 4133  df-neg 4135  df-div 4216  df-le 4277  df-n 4423  df-2 4462  df-n0 4535  df-z 4564  df-seq 4661  df-exp 4676

metamath.org