Theorem inar1 10186

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 10101	. . . . . 6 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
2		winaon 10099	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On)
3	1, 2	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ On)
4		winalim 10106	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → Lim 𝐴)
5	1, 4	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → Lim 𝐴)
6		r1lim 9185	. . . . 5 ⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
7	3, 5, 6	syl2anc 587	. . . 4 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
8		onelon 6184	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
9	3, 8	sylan 583	. . . . . . . 8 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
10		eleq1 2877	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
11		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑅1‘𝑥) = (𝑅1‘∅))
12	11	breq1d 5040	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘∅) ≺ 𝐴))
13	10, 12	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴)))
14		eleq1 2877	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
15		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
16	15	breq1d 5040	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
17	14, 16	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)))
18		eleq1 2877	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴))
19		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
20	19	breq1d 5040	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘suc 𝑦) ≺ 𝐴))
21	18, 20	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
22		ne0i 4250	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝐴 → 𝐴 ≠ ∅)
23		0sdomg 8630	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ On → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
24	22, 23	syl5ibr 249	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ≺ 𝐴))
25		r10 9181	. . . . . . . . . . . . 13 ⊢ (𝑅1‘∅) = ∅
26	25	breq1i 5037	. . . . . . . . . . . 12 ⊢ ((𝑅1‘∅) ≺ 𝐴 ↔ ∅ ≺ 𝐴)
27	24, 26	syl6ibr 255	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
28	1, 2, 27	3syl 18	. . . . . . . . . 10 ⊢ (𝐴 ∈ Inacc → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
29		eloni 6169	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → Ord 𝐴)
30		ordtr 6173	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝐴 → Tr 𝐴)
31	29, 30	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ On → Tr 𝐴)
32		trsuc 6243	. . . . . . . . . . . . . . 15 ⊢ ((Tr 𝐴 ∧ suc 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
33	32	ex 416	. . . . . . . . . . . . . 14 ⊢ (Tr 𝐴 → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
34	3, 31, 33	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Inacc → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
35	34	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
36		r1suc 9183	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) = 𝒫 (𝑅1‘𝑦))
37		fvex 6658	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅1‘𝑦) ∈ V
38	37	cardid 9958	. . . . . . . . . . . . . . . . 17 ⊢ (card‘(𝑅1‘𝑦)) ≈ (𝑅1‘𝑦)
39	38	ensymi 8542	. . . . . . . . . . . . . . . 16 ⊢ (𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦))
40		pwen 8674	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦)) → 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦))
42	36, 41	eqbrtrdi 5069	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
43		winacard 10103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
44	43	eleq2d 2875	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
45		cardsdom 9966	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅1‘𝑦) ∈ V ∧ 𝐴 ∈ On) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
46	37, 2, 45	sylancr 590	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
47	44, 46	bitr3d 284	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
48	1, 47	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Inacc → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
49		elina 10098	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴))
50	49	simp3bi 1144	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inacc → ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴)
51		pweq 4513	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → 𝒫 𝑧 = 𝒫 (card‘(𝑅1‘𝑦)))
52	51	breq1d 5040	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → (𝒫 𝑧 ≺ 𝐴 ↔ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
53	52	rspccv 3568	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴 → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
54	50, 53	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Inacc → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
55	48, 54	sylbird 263	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Inacc → ((𝑅1‘𝑦) ≺ 𝐴 → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
56	55	imp 410	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Inacc ∧ (𝑅1‘𝑦) ≺ 𝐴) → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴)
57		ensdomtr 8637	. . . . . . . . . . . . . 14 ⊢ (((𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)) ∧ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴) → (𝑅1‘suc 𝑦) ≺ 𝐴)
58	42, 56, 57	syl2an 598	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ On ∧ (𝐴 ∈ Inacc ∧ (𝑅1‘𝑦) ≺ 𝐴)) → (𝑅1‘suc 𝑦) ≺ 𝐴)
59	58	expr 460	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑅1‘𝑦) ≺ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))
60	35, 59	imim12d 81	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
61	60	ex 416	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (𝐴 ∈ Inacc → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))))
62		vex 3444	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
63		r1lim 9185	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
64	62, 63	mpan 689	. . . . . . . . . . . . . . 15 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
65		nfcv 2955	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝑧
66		nfcv 2955	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑅1‘𝑧)
67		nfcv 2955	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦 ≼
68		nfiu1 4915	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
69	66, 67, 68	nfbr 5077	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦(𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
70		fveq2 6645	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑧 → (𝑅1‘𝑦) = (𝑅1‘𝑧))
71	70	breq1d 5040	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → ((𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
72		fvex 6658	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (card‘(𝑅1‘𝑦)) ∈ V
73	62, 72	iunex 7651	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ V
74		ssiun2 4934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
75		ssdomg 8538	. . . . . . . . . . . . . . . . . . . . 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 8550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦)) ∧ (card‘(𝑅1‘𝑦)) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
78	39, 76, 77	sylancr 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
79	65, 69, 71, 78	vtoclgaf 3521	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑥 → (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
80	79	rgen 3116	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
81		iundom 9953	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
82	62, 80, 81	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
83	62, 73	unex 7449	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V
84		ssun2 4100	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
85		ssdomg 8538	. . . . . . . . . . . . . . . . . . . 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 8595	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
88	86, 87	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
89		ssun1 4099	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
90		ssdomg 8538	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
91	83, 89, 90	mp2 9	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
92	83	xpdom1 8599	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
94		domtr 8545	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ∧ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
95	88, 93, 94	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
96		limomss 7565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑥 → ω ⊆ 𝑥)
97	96, 89	sstrdi 3927	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝑥 → ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
98		ssdomg 8538	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
99	83, 97, 98	mpsyl 68	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑥 → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
100		infxpidm 9973	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
101	99, 100	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑥 → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
102		domentr 8551	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ∧ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
103	95, 101, 102	sylancr 590	. . . . . . . . . . . . . . . 16 ⊢ (Lim 𝑥 → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
104		domtr 8545	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∧ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
105	82, 103, 104	sylancr 590	. . . . . . . . . . . . . . 15 ⊢ (Lim 𝑥 → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
106	64, 105	eqbrtrd 5052	. . . . . . . . . . . . . 14 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
107	106	ad2antlr 726	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
108		eleq1a 2885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 → (𝐴 = 𝑥 → 𝐴 ∈ 𝐴))
109		ordirr 6177	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)
110	3, 29, 109	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Inacc → ¬ 𝐴 ∈ 𝐴)
111	108, 110	nsyli 160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → (𝐴 ∈ Inacc → ¬ 𝐴 = 𝑥))
112	111	imp 410	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ Inacc) → ¬ 𝐴 = 𝑥)
113	112	ad2ant2r 746	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = 𝑥)
114		simpll 766	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ 𝐴)
115		limord 6218	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Lim 𝑥 → Ord 𝑥)
116	62	elon 6168	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ Ord 𝑥)
117	115, 116	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑥 → 𝑥 ∈ On)
118	117	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ On)
119		cardf 9961	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ card:V⟶On
120		r1fnon 9180	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑅1 Fn On
121		dffn2 6489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅1 Fn On ↔ 𝑅1:On⟶V)
122	120, 121	mpbi 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅1:On⟶V
123		fco 6505	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((card:V⟶On ∧ 𝑅1:On⟶V) → (card ∘ 𝑅1):On⟶On)
124	119, 122, 123	mp2an 691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (card ∘ 𝑅1):On⟶On
125		onss 7485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
126		fssres 6518	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((card ∘ 𝑅1):On⟶On ∧ 𝑥 ⊆ On) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
127	124, 125, 126	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
128		ffn 6487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
129	118, 127, 128	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
130	3	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On)
131		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
132		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝐴)
133		ontr1 6205	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
134	133	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ On ∧ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) → 𝑦 ∈ 𝐴)
135	130, 131, 132, 134	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
136	37, 130, 45	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
137	1, 43	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐴 ∈ Inacc → (card‘𝐴) = 𝐴)
138	137	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (card‘𝐴) = 𝐴)
139	138	eleq2d 2875	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
140	136, 139	bitr3d 284	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑦) ≺ 𝐴 ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
141	140	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑦) ≺ 𝐴 → (card‘(𝑅1‘𝑦)) ∈ 𝐴))
142	135, 141	embantd 59	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (card‘(𝑅1‘𝑦)) ∈ 𝐴))
143	117	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → 𝑥 ∈ On)
144		fvres 6664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ 𝑥 → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
145	144	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
146		onelon 6184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
147		fvco3 6737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅1:On⟶V ∧ 𝑦 ∈ On) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
148	122, 146, 147	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
149	145, 148	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1‘𝑦)))
150	143, 149	sylan 583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1‘𝑦)))
151	150	eleq1d 2874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴 ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
152	142, 151	sylibrd 262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
153	152	ralimdva 3144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
154	153	impr 458	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴)
155		ffnfv 6859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ↔ (((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
156	129, 154, 155	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴)
157		eleq2 2878	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
158	157	biimpa 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
159		eliun 4885	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ ∃𝑦 ∈ 𝑥 𝑧 ∈ (card‘(𝑅1‘𝑦)))
160		cardon 9357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (card‘(𝑅1‘𝑦)) ∈ On
161	160	onelssi 6267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (card‘(𝑅1‘𝑦)))
162	149	sseq2d 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ↔ 𝑧 ⊆ (card‘(𝑅1‘𝑦))))
163	161, 162	syl5ibr 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
164	163	reximdva 3233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 𝑧 ∈ (card‘(𝑅1‘𝑦)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
165	159, 164	syl5bi 245	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ On → (𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
166	158, 165	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On → ((𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
167	166	expdimp 456	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
168	167	ralrimiv 3148	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
169	168	ex 416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
170	118, 169	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
171		ffun 6490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((card ∘ 𝑅1):On⟶On → Fun (card ∘ 𝑅1))
172	124, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (card ∘ 𝑅1)
173		resfunexg 6955	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (card ∘ 𝑅1) ∧ 𝑥 ∈ V) → ((card ∘ 𝑅1) ↾ 𝑥) ∈ V)
174	172, 62, 173	mp2an 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((card ∘ 𝑅1) ↾ 𝑥) ∈ V
175		feq1 6468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤:𝑥⟶𝐴 ↔ ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴))
176		fveq1 6644	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤‘𝑦) = (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
177	176	sseq2d 3947	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑧 ⊆ (𝑤‘𝑦) ↔ 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
178	177	rexbidv 3256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
179	178	ralbidv 3162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
180	175, 179	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → ((𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) ↔ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))))
181	174, 180	spcev 3555	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)))
182	156, 170, 181	syl6an 683	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦))))
183	3	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝐴 ∈ On)
184		cfflb 9670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
185	183, 118, 184	syl2anc 587	. . . . . . . . . . . . . . . . . . . 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 3946	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ Inacc → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
189	188	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
190	186, 189	sylibd 242	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → 𝐴 ⊆ 𝑥))
191		ontri1 6193	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴))
192	183, 118, 191	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴))
193	190, 192	sylibd 242	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ¬ 𝑥 ∈ 𝐴))
194	114, 193	mt2d 138	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
195		iunon 7959	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
196	62, 195	mpan 689	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
197	160	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ∈ On)
198	196, 197	mprg 3120	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On
199		eqcom 2805	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 ↔ 𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
200		eloni 6169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → Ord 𝑥)
201		eloni 6169	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → Ord ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
202		ordequn 6259	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord 𝑥 ∧ Ord ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
203	200, 201, 202	syl2an 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → (𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
204	199, 203	syl5bi 245	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
205	118, 198, 204	sylancl 589	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
206	113, 194, 205	mtord 877	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)
207		onelss 6201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
208	183, 114, 207	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ⊆ 𝐴)
209		onelss 6201	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∈ On → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
210	130, 142, 209	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
211	210	ralimdva 3144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
212	211	impr 458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
213		iunss 4932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
214	212, 213	sylibr 237	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
215	208, 214	unssd 4113	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴)
216		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → 𝑥 = if(𝑥 ∈ On, 𝑥, ∅))
217		iuneq1 4897	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) = ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)))
218	216, 217	uneq12d 4091	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))))
219	218	eleq1d 2874	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On ↔ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))) ∈ On))
220		0elon 6212	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∅ ∈ On
221	220	elimel 4492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ On
222	221	elexi 3460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ V
223		iunon 7959	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((if(𝑥 ∈ On, 𝑥, ∅) ∈ V ∧ ∀𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On)
224	222, 223	mpan 689	. . . . . . . . . . . . . . . . . . . . . . . 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 3120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On
227	221, 226	onun2i 6274	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))) ∈ On
228	219, 227	dedth 4481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
229	117, 228	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑥 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
230	229	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ Lim 𝑥) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
231	3	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)) → 𝐴 ∈ On)
232		onsseleq 6200	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On ∧ 𝐴 ∈ On) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴 ↔ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)))
233	230, 231, 232	syl2an 598	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴 ↔ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)))
234	215, 233	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴))
235	234	orcomd 868	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴))
236	235	ord 861	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (¬ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴))
237	206, 236	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴)
238	137	ad2antrl 727	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (card‘𝐴) = 𝐴)
239		iscard 9388	. . . . . . . . . . . . . . . 16 ⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴))
240	239	simprbi 500	. . . . . . . . . . . . . . 15 ⊢ ((card‘𝐴) = 𝐴 → ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴)
241		breq1 5033	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑧 ≺ 𝐴 ↔ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴))
242	241	rspccv 3568	. . . . . . . . . . . . . . 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 8636	. . . . . . . . . . . . 13 ⊢ (((𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∧ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
246	107, 244, 245	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑅1‘𝑥) ≺ 𝐴)
247	246	exp43 440	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴))))
248	247	com4l 92	. . . . . . . . . 10 ⊢ (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴))))
249	13, 17, 21, 28, 61, 248	tfinds2 7558	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (𝐴 ∈ Inacc → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴)))
250	249	impd 414	. . . . . . . 8 ⊢ (𝑥 ∈ On → ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴))
251	9, 250	mpcom 38	. . . . . . 7 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
252		sdomdom 8520	. . . . . . 7 ⊢ ((𝑅1‘𝑥) ≺ 𝐴 → (𝑅1‘𝑥) ≼ 𝐴)
253	251, 252	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≼ 𝐴)
254	253	ralrimiva 3149	. . . . 5 ⊢ (𝐴 ∈ Inacc → ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴)
255		iundom 9953	. . . . 5 ⊢ ((𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴) → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
256	3, 254, 255	syl2anc 587	. . . 4 ⊢ (𝐴 ∈ Inacc → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
257	7, 256	eqbrtrd 5052	. . 3 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ (𝐴 × 𝐴))
258		winainf 10105	. . . . 5 ⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
259	1, 258	syl 17	. . . 4 ⊢ (𝐴 ∈ Inacc → ω ⊆ 𝐴)
260		infxpen 9425	. . . 4 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
261	3, 259, 260	syl2anc 587	. . 3 ⊢ (𝐴 ∈ Inacc → (𝐴 × 𝐴) ≈ 𝐴)
262		domentr 8551	. . 3 ⊢ (((𝑅1‘𝐴) ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≈ 𝐴) → (𝑅1‘𝐴) ≼ 𝐴)
263	257, 261, 262	syl2anc 587	. 2 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ 𝐴)
264		fvex 6658	. . 3 ⊢ (𝑅1‘𝐴) ∈ V
265	122	fdmi 6498	. . . . 5 ⊢ dom 𝑅1 = On
266	2, 265	eleqtrrdi 2901	. . . 4 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ dom 𝑅1)
267		onssr1 9244	. . . 4 ⊢ (𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴))
268	1, 266, 267	3syl 18	. . 3 ⊢ (𝐴 ∈ Inacc → 𝐴 ⊆ (𝑅1‘𝐴))
269		ssdomg 8538	. . 3 ⊢ ((𝑅1‘𝐴) ∈ V → (𝐴 ⊆ (𝑅1‘𝐴) → 𝐴 ≼ (𝑅1‘𝐴)))
270	264, 268, 269	mpsyl 68	. 2 ⊢ (𝐴 ∈ Inacc → 𝐴 ≼ (𝑅1‘𝐴))
271		sbth 8621	. 2 ⊢ (((𝑅1‘𝐴) ≼ 𝐴 ∧ 𝐴 ≼ (𝑅1‘𝐴)) → (𝑅1‘𝐴) ≈ 𝐴)
272	263, 270, 271	syl2anc 587	1 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  ifcif 4425  𝒫 cpw 4497  ∪ ciun 4881   class class class wbr 5030  Tr wtr 5136   × cxp 5517  dom cdm 5519   ↾ cres 5521   ∘ ccom 5523  Ord word 6158  Oncon0 6159  Lim wlim 6160  suc csuc 6161  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  ωcom 7560   ≈ cen 8489   ≼ cdom 8490   ≺ csdm 8491  𝑅₁cr1 9175  cardccrd 9348  cfccf 9350  Inacc_wcwina 10093  Inacccina 10094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-ac2 9874

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-oi 8958  df-r1 9177  df-rank 9178  df-card 9352  df-cf 9354  df-acn 9355  df-ac 9527  df-wina 10095  df-ina 10096

This theorem is referenced by:  r1omALT  10187  inatsk  10189