Theorem inar1 10804

Description: (𝑅₁‘𝐴) for 𝐴 a strongly inaccessible cardinal is equipotent to 𝐴. (Contributed by Mario Carneiro, 6-Jun-2013.)

Assertion

Ref	Expression
inar1	⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴)

Proof of Theorem inar1

Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inawina 10719	. . . . . 6 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
2		winaon 10717	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On)
3	1, 2	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ On)
4		winalim 10724	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → Lim 𝐴)
5	1, 4	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → Lim 𝐴)
6		r1lim 9801	. . . . 5 ⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
7	3, 5, 6	syl2anc 582	. . . 4 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
8		onelon 6397	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
9	3, 8	sylan 578	. . . . . . . 8 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
10		eleq1 2816	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
11		fveq2 6900	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑅1‘𝑥) = (𝑅1‘∅))
12	11	breq1d 5160	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘∅) ≺ 𝐴))
13	10, 12	imbi12d 343	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴)))
14		eleq1 2816	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
15		fveq2 6900	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
16	15	breq1d 5160	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
17	14, 16	imbi12d 343	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)))
18		eleq1 2816	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴))
19		fveq2 6900	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
20	19	breq1d 5160	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘suc 𝑦) ≺ 𝐴))
21	18, 20	imbi12d 343	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
22		ne0i 4336	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝐴 → 𝐴 ≠ ∅)
23		0sdomg 9133	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ On → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
24	22, 23	imbitrrid 245	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ≺ 𝐴))
25		r10 9797	. . . . . . . . . . . . 13 ⊢ (𝑅1‘∅) = ∅
26	25	breq1i 5157	. . . . . . . . . . . 12 ⊢ ((𝑅1‘∅) ≺ 𝐴 ↔ ∅ ≺ 𝐴)
27	24, 26	imbitrrdi 251	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
28	1, 2, 27	3syl 18	. . . . . . . . . 10 ⊢ (𝐴 ∈ Inacc → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
29		eloni 6382	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → Ord 𝐴)
30		ordtr 6386	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝐴 → Tr 𝐴)
31	29, 30	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ On → Tr 𝐴)
32		trsuc 6459	. . . . . . . . . . . . . . 15 ⊢ ((Tr 𝐴 ∧ suc 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
33	32	ex 411	. . . . . . . . . . . . . 14 ⊢ (Tr 𝐴 → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
34	3, 31, 33	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Inacc → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
35	34	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
36		r1suc 9799	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) = 𝒫 (𝑅1‘𝑦))
37		fvex 6913	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅1‘𝑦) ∈ V
38	37	cardid 10576	. . . . . . . . . . . . . . . . 17 ⊢ (card‘(𝑅1‘𝑦)) ≈ (𝑅1‘𝑦)
39	38	ensymi 9029	. . . . . . . . . . . . . . . 16 ⊢ (𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦))
40		pwen 9179	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦)) → 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦))
42	36, 41	eqbrtrdi 5189	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
43		winacard 10721	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
44	43	eleq2d 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
45		cardsdom 10584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅1‘𝑦) ∈ V ∧ 𝐴 ∈ On) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
46	37, 2, 45	sylancr 585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
47	44, 46	bitr3d 280	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
48	1, 47	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Inacc → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
49		elina 10716	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴))
50	49	simp3bi 1144	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inacc → ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴)
51		pweq 4618	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → 𝒫 𝑧 = 𝒫 (card‘(𝑅1‘𝑦)))
52	51	breq1d 5160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → (𝒫 𝑧 ≺ 𝐴 ↔ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
53	52	rspccv 3606	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴 → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
54	50, 53	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Inacc → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
55	48, 54	sylbird 259	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Inacc → ((𝑅1‘𝑦) ≺ 𝐴 → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
56	55	imp 405	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Inacc ∧ (𝑅1‘𝑦) ≺ 𝐴) → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴)
57		ensdomtr 9142	. . . . . . . . . . . . . 14 ⊢ (((𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)) ∧ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴) → (𝑅1‘suc 𝑦) ≺ 𝐴)
58	42, 56, 57	syl2an 594	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ On ∧ (𝐴 ∈ Inacc ∧ (𝑅1‘𝑦) ≺ 𝐴)) → (𝑅1‘suc 𝑦) ≺ 𝐴)
59	58	expr 455	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑅1‘𝑦) ≺ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))
60	35, 59	imim12d 81	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
61	60	ex 411	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (𝐴 ∈ Inacc → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))))
62		vex 3475	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
63		r1lim 9801	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
64	62, 63	mpan 688	. . . . . . . . . . . . . . 15 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
65		nfcv 2898	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝑧
66		nfcv 2898	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑅1‘𝑧)
67		nfcv 2898	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦 ≼
68		nfiu1 5032	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
69	66, 67, 68	nfbr 5197	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦(𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
70		fveq2 6900	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑧 → (𝑅1‘𝑦) = (𝑅1‘𝑧))
71	70	breq1d 5160	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → ((𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
72		fvex 6913	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (card‘(𝑅1‘𝑦)) ∈ V
73	62, 72	iunex 7976	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ V
74		ssiun2 5052	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
75		ssdomg 9025	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ V → ((card‘(𝑅1‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → (card‘(𝑅1‘𝑦)) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
76	73, 74, 75	mpsyl 68	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
77		endomtr 9037	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦)) ∧ (card‘(𝑅1‘𝑦)) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
78	39, 76, 77	sylancr 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
79	65, 69, 71, 78	vtoclgaf 3562	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑥 → (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
80	79	rgen 3059	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
81		iundom 10571	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
82	62, 80, 81	mp2an 690	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
83	62, 73	unex 7752	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V
84		ssun2 4173	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
85		ssdomg 9025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
86	83, 84, 85	mp2 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
87	62	xpdom2 9096	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
88	86, 87	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
89		ssun1 4172	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
90		ssdomg 9025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
91	83, 89, 90	mp2 9	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
92	83	xpdom1 9100	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
94		domtr 9032	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ∧ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
95	88, 93, 94	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
96		limomss 7879	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑥 → ω ⊆ 𝑥)
97	96, 89	sstrdi 3992	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝑥 → ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
98		ssdomg 9025	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
99	83, 97, 98	mpsyl 68	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑥 → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
100		infxpidm 10591	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
101	99, 100	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑥 → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
102		domentr 9038	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ∧ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
103	95, 101, 102	sylancr 585	. . . . . . . . . . . . . . . 16 ⊢ (Lim 𝑥 → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
104		domtr 9032	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∧ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
105	82, 103, 104	sylancr 585	. . . . . . . . . . . . . . 15 ⊢ (Lim 𝑥 → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
106	64, 105	eqbrtrd 5172	. . . . . . . . . . . . . 14 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
107	106	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
108		eleq1a 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 → (𝐴 = 𝑥 → 𝐴 ∈ 𝐴))
109		ordirr 6390	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)
110	3, 29, 109	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Inacc → ¬ 𝐴 ∈ 𝐴)
111	108, 110	nsyli 157	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → (𝐴 ∈ Inacc → ¬ 𝐴 = 𝑥))
112	111	imp 405	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ Inacc) → ¬ 𝐴 = 𝑥)
113	112	ad2ant2r 745	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = 𝑥)
114		simpll 765	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ 𝐴)
115		limord 6432	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Lim 𝑥 → Ord 𝑥)
116	62	elon 6381	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ Ord 𝑥)
117	115, 116	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑥 → 𝑥 ∈ On)
118	117	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ On)
119		cardf 10579	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ card:V⟶On
120		r1fnon 9796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑅1 Fn On
121		dffn2 6727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅1 Fn On ↔ 𝑅1:On⟶V)
122	120, 121	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅1:On⟶V
123		fco 6750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((card:V⟶On ∧ 𝑅1:On⟶V) → (card ∘ 𝑅1):On⟶On)
124	119, 122, 123	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (card ∘ 𝑅1):On⟶On
125		onss 7791	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
126		fssres 6766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((card ∘ 𝑅1):On⟶On ∧ 𝑥 ⊆ On) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
127	124, 125, 126	sylancr 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
128		ffn 6725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
129	118, 127, 128	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
130	3	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On)
131		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
132		simplll 773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝐴)
133		ontr1 6418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
134	133	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ On ∧ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) → 𝑦 ∈ 𝐴)
135	130, 131, 132, 134	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
136	37, 130, 45	sylancr 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
137	1, 43	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐴 ∈ Inacc → (card‘𝐴) = 𝐴)
138	137	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (card‘𝐴) = 𝐴)
139	138	eleq2d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
140	136, 139	bitr3d 280	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑦) ≺ 𝐴 ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
141	140	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑦) ≺ 𝐴 → (card‘(𝑅1‘𝑦)) ∈ 𝐴))
142	135, 141	embantd 59	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (card‘(𝑅1‘𝑦)) ∈ 𝐴))
143	117	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → 𝑥 ∈ On)
144		fvres 6919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ 𝑥 → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
145	144	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
146		onelon 6397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
147		fvco3 7000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅1:On⟶V ∧ 𝑦 ∈ On) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
148	122, 146, 147	sylancr 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
149	145, 148	eqtrd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1‘𝑦)))
150	143, 149	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1‘𝑦)))
151	150	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴 ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
152	142, 151	sylibrd 258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
153	152	ralimdva 3163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
154	153	impr 453	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴)
155		ffnfv 7132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ↔ (((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
156	129, 154, 155	sylanbrc 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴)
157		eleq2 2817	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
158	157	biimpa 475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
159		eliun 5002	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ ∃𝑦 ∈ 𝑥 𝑧 ∈ (card‘(𝑅1‘𝑦)))
160		cardon 9973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (card‘(𝑅1‘𝑦)) ∈ On
161	160	onelssi 6487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (card‘(𝑅1‘𝑦)))
162	149	sseq2d 4012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ↔ 𝑧 ⊆ (card‘(𝑅1‘𝑦))))
163	161, 162	imbitrrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
164	163	reximdva 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 𝑧 ∈ (card‘(𝑅1‘𝑦)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
165	159, 164	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ On → (𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
166	158, 165	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On → ((𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
167	166	expdimp 451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
168	167	ralrimiv 3141	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
169	168	ex 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
170	118, 169	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
171		ffun 6728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((card ∘ 𝑅1):On⟶On → Fun (card ∘ 𝑅1))
172	124, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (card ∘ 𝑅1)
173		resfunexg 7231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (card ∘ 𝑅1) ∧ 𝑥 ∈ V) → ((card ∘ 𝑅1) ↾ 𝑥) ∈ V)
174	172, 62, 173	mp2an 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((card ∘ 𝑅1) ↾ 𝑥) ∈ V
175		feq1 6706	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤:𝑥⟶𝐴 ↔ ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴))
176		fveq1 6899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤‘𝑦) = (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
177	176	sseq2d 4012	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑧 ⊆ (𝑤‘𝑦) ↔ 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
178	177	rexbidv 3174	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
179	178	ralbidv 3173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
180	175, 179	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → ((𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) ↔ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))))
181	174, 180	spcev 3593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)))
182	156, 170, 181	syl6an 682	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦))))
183	3	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝐴 ∈ On)
184		cfflb 10288	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
185	183, 118, 184	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
186	182, 185	syld 47	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
187	49	simp2bi 1143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ Inacc → (cf‘𝐴) = 𝐴)
188	187	sseq1d 4011	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ Inacc → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
189	188	ad2antrl 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
190	186, 189	sylibd 238	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → 𝐴 ⊆ 𝑥))
191		ontri1 6406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴))
192	183, 118, 191	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴))
193	190, 192	sylibd 238	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ¬ 𝑥 ∈ 𝐴))
194	114, 193	mt2d 136	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
195		iunon 8364	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
196	62, 195	mpan 688	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
197	160	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ∈ On)
198	196, 197	mprg 3063	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On
199		eqcom 2734	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 ↔ 𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
200		eloni 6382	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → Ord 𝑥)
201		eloni 6382	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → Ord ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
202		ordequn 6475	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord 𝑥 ∧ Ord ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
203	200, 201, 202	syl2an 594	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → (𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
204	199, 203	biimtrid 241	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
205	118, 198, 204	sylancl 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
206	113, 194, 205	mtord 877	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)
207		onelss 6414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
208	183, 114, 207	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ⊆ 𝐴)
209		onelss 6414	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∈ On → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
210	130, 142, 209	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
211	210	ralimdva 3163	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
212	211	impr 453	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
213		iunss 5050	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
214	212, 213	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
215	208, 214	unssd 4186	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴)
216		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → 𝑥 = if(𝑥 ∈ On, 𝑥, ∅))
217		iuneq1 5014	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) = ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)))
218	216, 217	uneq12d 4163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))))
219	218	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On ↔ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))) ∈ On))
220		0elon 6426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∅ ∈ On
221	220	elimel 4599	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ On
222	221	elexi 3491	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ V
223		iunon 8364	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((if(𝑥 ∈ On, 𝑥, ∅) ∈ V ∧ ∀𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On)
224	222, 223	mpan 688	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On → ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On)
225	160	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ if(𝑥 ∈ On, 𝑥, ∅) → (card‘(𝑅1‘𝑦)) ∈ On)
226	224, 225	mprg 3063	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On
227	221, 226	onun2i 6494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))) ∈ On
228	219, 227	dedth 4588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
229	117, 228	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑥 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
230	229	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ Lim 𝑥) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
231	3	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)) → 𝐴 ∈ On)
232		onsseleq 6413	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On ∧ 𝐴 ∈ On) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴 ↔ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)))
233	230, 231, 232	syl2an 594	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴 ↔ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)))
234	215, 233	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴))
235	234	orcomd 869	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴))
236	235	ord 862	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (¬ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴))
237	206, 236	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴)
238	137	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (card‘𝐴) = 𝐴)
239		iscard 10004	. . . . . . . . . . . . . . . 16 ⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴))
240	239	simprbi 495	. . . . . . . . . . . . . . 15 ⊢ ((card‘𝐴) = 𝐴 → ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴)
241		breq1 5153	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑧 ≺ 𝐴 ↔ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴))
242	241	rspccv 3606	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴 → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴))
243	238, 240, 242	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴))
244	237, 243	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴)
245		domsdomtr 9141	. . . . . . . . . . . . 13 ⊢ (((𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∧ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
246	107, 244, 245	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑅1‘𝑥) ≺ 𝐴)
247	246	exp43 435	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴))))
248	247	com4l 92	. . . . . . . . . 10 ⊢ (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴))))
249	13, 17, 21, 28, 61, 248	tfinds2 7872	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (𝐴 ∈ Inacc → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴)))
250	249	impd 409	. . . . . . . 8 ⊢ (𝑥 ∈ On → ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴))
251	9, 250	mpcom 38	. . . . . . 7 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
252		sdomdom 9005	. . . . . . 7 ⊢ ((𝑅1‘𝑥) ≺ 𝐴 → (𝑅1‘𝑥) ≼ 𝐴)
253	251, 252	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≼ 𝐴)
254	253	ralrimiva 3142	. . . . 5 ⊢ (𝐴 ∈ Inacc → ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴)
255		iundom 10571	. . . . 5 ⊢ ((𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴) → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
256	3, 254, 255	syl2anc 582	. . . 4 ⊢ (𝐴 ∈ Inacc → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
257	7, 256	eqbrtrd 5172	. . 3 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ (𝐴 × 𝐴))
258		winainf 10723	. . . . 5 ⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
259	1, 258	syl 17	. . . 4 ⊢ (𝐴 ∈ Inacc → ω ⊆ 𝐴)
260		infxpen 10043	. . . 4 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
261	3, 259, 260	syl2anc 582	. . 3 ⊢ (𝐴 ∈ Inacc → (𝐴 × 𝐴) ≈ 𝐴)
262		domentr 9038	. . 3 ⊢ (((𝑅1‘𝐴) ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≈ 𝐴) → (𝑅1‘𝐴) ≼ 𝐴)
263	257, 261, 262	syl2anc 582	. 2 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ 𝐴)
264		fvex 6913	. . 3 ⊢ (𝑅1‘𝐴) ∈ V
265	122	fdmi 6737	. . . . 5 ⊢ dom 𝑅1 = On
266	2, 265	eleqtrrdi 2839	. . . 4 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ dom 𝑅1)
267		onssr1 9860	. . . 4 ⊢ (𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴))
268	1, 266, 267	3syl 18	. . 3 ⊢ (𝐴 ∈ Inacc → 𝐴 ⊆ (𝑅1‘𝐴))
269		ssdomg 9025	. . 3 ⊢ ((𝑅1‘𝐴) ∈ V → (𝐴 ⊆ (𝑅1‘𝐴) → 𝐴 ≼ (𝑅1‘𝐴)))
270	264, 268, 269	mpsyl 68	. 2 ⊢ (𝐴 ∈ Inacc → 𝐴 ≼ (𝑅1‘𝐴))
271		sbth 9122	. 2 ⊢ (((𝑅1‘𝐴) ≼ 𝐴 ∧ 𝐴 ≼ (𝑅1‘𝐴)) → (𝑅1‘𝐴) ≈ 𝐴)
272	263, 270, 271	syl2anc 582	1 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ≠ wne 2936  ∀wral 3057  ∃wrex 3066  Vcvv 3471   ∪ cun 3945   ⊆ wss 3947  ∅c0 4324  ifcif 4530  𝒫 cpw 4604  ∪ ciun 4998   class class class wbr 5150  Tr wtr 5267   × cxp 5678  dom cdm 5680   ↾ cres 5682   ∘ ccom 5684  Ord word 6371  Oncon0 6372  Lim wlim 6373  suc csuc 6374  Fun wfun 6545   Fn wfn 6546  ⟶wf 6547  ‘cfv 6551  ωcom 7874   ≈ cen 8965   ≼ cdom 8966   ≺ csdm 8967  𝑅₁cr1 9791  cardccrd 9964  cfccf 9966  Inacc_wcwina 10711  Inacccina 10712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-inf2 9670  ax-ac2 10492

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-int 4952  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-se 5636  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-isom 6560  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7875  df-1st 7997  df-2nd 7998  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-1o 8491  df-2o 8492  df-er 8729  df-map 8851  df-en 8969  df-dom 8970  df-sdom 8971  df-fin 8972  df-oi 9539  df-r1 9793  df-rank 9794  df-card 9968  df-cf 9970  df-acn 9971  df-ac 10145  df-wina 10713  df-ina 10714

This theorem is referenced by:  r1omALT  10805  inatsk  10807