Theorem cfslb2n 10350

Description: Any small collection of small subsets of 𝐴 cannot have union 𝐴, where "small" means smaller than the cofinality. This is a stronger version of cfslb 10348. This is a common application of cofinality: under AC, (ℵ‘1) is regular, so it is not a countable union of countable sets. (Contributed by Mario Carneiro, 24-Jun-2013.)

Hypothesis

Ref	Expression
cfslb.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
cfslb2n	⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (𝐵 ≺ (cf‘𝐴) → ∪ 𝐵 ≠ 𝐴))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem cfslb2n

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		limord 6424	. . . . . . . . . 10 ⊢ (Lim 𝐴 → Ord 𝐴)
2		ordsson 7798	. . . . . . . . . 10 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
3		sstr 3916	. . . . . . . . . . 11 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑥 ⊆ On)
4	3	expcom 419	. . . . . . . . . 10 ⊢ (𝐴 ⊆ On → (𝑥 ⊆ 𝐴 → 𝑥 ⊆ On))
5	1, 2, 4	3syl 19	. . . . . . . . 9 ⊢ (Lim 𝐴 → (𝑥 ⊆ 𝐴 → 𝑥 ⊆ On))
6		onsucuni 7840	. . . . . . . . 9 ⊢ (𝑥 ⊆ On → 𝑥 ⊆ suc ∪ 𝑥)
7	5, 6	syl6 36	. . . . . . . 8 ⊢ (Lim 𝐴 → (𝑥 ⊆ 𝐴 → 𝑥 ⊆ suc ∪ 𝑥))
8	7	adantrd 497	. . . . . . 7 ⊢ (Lim 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → 𝑥 ⊆ suc ∪ 𝑥))
9	8	ralimdv 3176	. . . . . 6 ⊢ (Lim 𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∀𝑥 ∈ 𝐵 𝑥 ⊆ suc ∪ 𝑥))
10		uniiun 5016	. . . . . . 7 ⊢ ∪ 𝐵 = ∪ 𝑥 ∈ 𝐵 𝑥
11		ss2iun 4969	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 𝑥 ⊆ suc ∪ 𝑥 → ∪ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥)
12	10, 11	eqsstrid 3946	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐵 𝑥 ⊆ suc ∪ 𝑥 → ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥)
13	9, 12	syl6 36	. . . . 5 ⊢ (Lim 𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥))
14	13	imp 412	. . . 4 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥)
15		cfslb.1	. . . . . . . . . 10 ⊢ 𝐴 ∈ V
16	15	cfslbn 10349	. . . . . . . . 9 ⊢ ((Lim 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∪ 𝑥 ∈ 𝐴)
17	16	3expib 1140	. . . . . . . 8 ⊢ (Lim 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∪ 𝑥 ∈ 𝐴))
18		ordsucss 7830	. . . . . . . 8 ⊢ (Ord 𝐴 → (∪ 𝑥 ∈ 𝐴 → suc ∪ 𝑥 ⊆ 𝐴))
19	1, 17, 18	sylsyld 62	. . . . . . 7 ⊢ (Lim 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → suc ∪ 𝑥 ⊆ 𝐴))
20	19	ralimdv 3176	. . . . . 6 ⊢ (Lim 𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴))
21		iunss 5002	. . . . . 6 ⊢ (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 ↔ ∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴)
22	20, 21	imbitrrdi 255	. . . . 5 ⊢ (Lim 𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴))
23	22	imp 412	. . . 4 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴)
24		sseq1 3933	. . . . . 6 ⊢ (∪ 𝐵 = 𝐴 → (∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ↔ 𝐴 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥))
25		eqss 3923	. . . . . . 7 ⊢ (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ↔ (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥))
26	25	simplbi2com 508	. . . . . 6 ⊢ (𝐴 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴))
27	24, 26	biimtrdi 256	. . . . 5 ⊢ (∪ 𝐵 = 𝐴 → (∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴)))
28	27	com3l 90	. . . 4 ⊢ (∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 → (∪ 𝐵 = 𝐴 → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴)))
29	14, 23, 28	sylc 66	. . 3 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (∪ 𝐵 = 𝐴 → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴))
30		limsuc 7861	. . . . . . . . 9 ⊢ (Lim 𝐴 → (∪ 𝑥 ∈ 𝐴 ↔ suc ∪ 𝑥 ∈ 𝐴))
31	17, 30	sylibd 242	. . . . . . . 8 ⊢ (Lim 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → suc ∪ 𝑥 ∈ 𝐴))
32	31	ralimdv 3176	. . . . . . 7 ⊢ (Lim 𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴))
33	32	imp 412	. . . . . 6 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → ∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴)
34		r19.29 3125	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥) → ∃𝑥 ∈ 𝐵 (suc ∪ 𝑥 ∈ 𝐴 ∧ 𝑦 = suc ∪ 𝑥))
35		eleq1 2848	. . . . . . . . . 10 ⊢ (𝑦 = suc ∪ 𝑥 → (𝑦 ∈ 𝐴 ↔ suc ∪ 𝑥 ∈ 𝐴))
36	35	biimparc 485	. . . . . . . . 9 ⊢ ((suc ∪ 𝑥 ∈ 𝐴 ∧ 𝑦 = suc ∪ 𝑥) → 𝑦 ∈ 𝐴)
37	36	rexlimivw 3159	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐵 (suc ∪ 𝑥 ∈ 𝐴 ∧ 𝑦 = suc ∪ 𝑥) → 𝑦 ∈ 𝐴)
38	34, 37	syl 18	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥) → 𝑦 ∈ 𝐴)
39	38	ex 418	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 → 𝑦 ∈ 𝐴))
40	33, 39	syl 18	. . . . 5 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 → 𝑦 ∈ 𝐴))
41	40	abssdv 3992	. . . 4 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ⊆ 𝐴)
42		vuniex 7757	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ V
43	42	sucex 7821	. . . . . . 7 ⊢ suc ∪ 𝑥 ∈ V
44	43	dfiun2 4989	. . . . . 6 ⊢ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥}
45	44	eqeq1i 2765	. . . . 5 ⊢ (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ↔ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} = 𝐴)
46	15	cfslb 10348	. . . . . 6 ⊢ ((Lim 𝐴 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ⊆ 𝐴 ∧ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} = 𝐴) → (cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥})
47	46	3expia 1139	. . . . 5 ⊢ ((Lim 𝐴 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ⊆ 𝐴) → (∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} = 𝐴 → (cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥}))
48	45, 47	biimtrid 245	. . . 4 ⊢ ((Lim 𝐴 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 → (cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥}))
49	41, 48	syldan 603	. . 3 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 → (cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥}))
50		eqid 2760	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) = (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥)
51	50	rnmpt 5938	. . . . . . . 8 ⊢ ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥}
52	43, 50	fnmpti 6683	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) Fn 𝐵
53		dffn4 6803	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) Fn 𝐵 ↔ (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥))
54	52, 53	mpbi 233	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥)
55		relsdom 8984	. . . . . . . . . . 11 ⊢ Rel ≺
56	55	brrelex1i 5706	. . . . . . . . . 10 ⊢ (𝐵 ≺ (cf‘𝐴) → 𝐵 ∈ V)
57		breq1 5105	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → (𝑦 ≺ (cf‘𝐴) ↔ 𝐵 ≺ (cf‘𝐴)))
58		foeq2 6794	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐵 → ((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ↔ (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥)))
59		breq2 5106	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐵 → (ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝑦 ↔ ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝐵))
60	58, 59	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → (((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝑦) ↔ ((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝐵)))
61	57, 60	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → ((𝑦 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝑦)) ↔ (𝐵 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝐵))))
62		cfon 10336	. . . . . . . . . . . . 13 ⊢ (cf‘𝐴) ∈ On
63		sdomdom 9011	. . . . . . . . . . . . 13 ⊢ (𝑦 ≺ (cf‘𝐴) → 𝑦 ≼ (cf‘𝐴))
64		ondomen 10120	. . . . . . . . . . . . 13 ⊢ (((cf‘𝐴) ∈ On ∧ 𝑦 ≼ (cf‘𝐴)) → 𝑦 ∈ dom card)
65	62, 63, 64	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑦 ≺ (cf‘𝐴) → 𝑦 ∈ dom card)
66		fodomnum 10140	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ dom card → ((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝑦))
67	65, 66	syl 18	. . . . . . . . . . 11 ⊢ (𝑦 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝑦))
68	61, 67	vtoclg 3517	. . . . . . . . . 10 ⊢ (𝐵 ∈ V → (𝐵 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝐵)))
69	56, 68	mpcom 39	. . . . . . . . 9 ⊢ (𝐵 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝐵))
70	54, 69	mpi 21	. . . . . . . 8 ⊢ (𝐵 ≺ (cf‘𝐴) → ran (𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥) ≼ 𝐵)
71	51, 70	eqbrtrrid 5140	. . . . . . 7 ⊢ (𝐵 ≺ (cf‘𝐴) → {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ≼ 𝐵)
72		domtr 9038	. . . . . . 7 ⊢ (((cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ≼ 𝐵) → (cf‘𝐴) ≼ 𝐵)
73	71, 72	sylan2 605	. . . . . 6 ⊢ (((cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ∧ 𝐵 ≺ (cf‘𝐴)) → (cf‘𝐴) ≼ 𝐵)
74		domnsym 9126	. . . . . 6 ⊢ ((cf‘𝐴) ≼ 𝐵 → ¬ 𝐵 ≺ (cf‘𝐴))
75	73, 74	syl 18	. . . . 5 ⊢ (((cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ∧ 𝐵 ≺ (cf‘𝐴)) → ¬ 𝐵 ≺ (cf‘𝐴))
76	75	pm2.01da 811	. . . 4 ⊢ ((cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} → ¬ 𝐵 ≺ (cf‘𝐴))
77	76	a1i 11	. . 3 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → ((cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} → ¬ 𝐵 ≺ (cf‘𝐴)))
78	29, 49, 77	3syld 61	. 2 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (∪ 𝐵 = 𝐴 → ¬ 𝐵 ≺ (cf‘𝐴)))
79	78	necon2ad 2970	1 ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (𝐵 ≺ (cf‘𝐴) → ∪ 𝐵 ≠ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {cab 2738   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3895  ∪ cuni 4866  ∪ ciun 4950   class class class wbr 5102   ↦ cmpt 5185  dom cdm 5650  ran crn 5651  Ord word 6361  Oncon0 6362  Lim wlim 6363  suc csuc 6364   Fn wfn 6534  –onto→wfo 6537  ‘cfv 6539   ≼ cdom 8975   ≺ csdm 8976  cardccrd 10020  cfccf 10022

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-isom 6548  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-1st 8002  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-er 8721  df-map 8853  df-en 8978  df-dom 8979  df-sdom 8980  df-card 10024  df-cf 10026  df-acn 10027

This theorem is used by:  tskuni  10872