Theorem inar1 10531

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 10446	. . . . . 6 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
2		winaon 10444	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On)
3	1, 2	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ On)
4		winalim 10451	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → Lim 𝐴)
5	1, 4	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → Lim 𝐴)
6		r1lim 9530	. . . . 5 ⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
7	3, 5, 6	syl2anc 584	. . . 4 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
8		onelon 6291	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
9	3, 8	sylan 580	. . . . . . . 8 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
10		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
11		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑅1‘𝑥) = (𝑅1‘∅))
12	11	breq1d 5084	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘∅) ≺ 𝐴))
13	10, 12	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴)))
14		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
15		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
16	15	breq1d 5084	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
17	14, 16	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)))
18		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴))
19		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
20	19	breq1d 5084	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘suc 𝑦) ≺ 𝐴))
21	18, 20	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
22		ne0i 4268	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝐴 → 𝐴 ≠ ∅)
23		0sdomg 8891	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ On → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
24	22, 23	syl5ibr 245	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ≺ 𝐴))
25		r10 9526	. . . . . . . . . . . . 13 ⊢ (𝑅1‘∅) = ∅
26	25	breq1i 5081	. . . . . . . . . . . 12 ⊢ ((𝑅1‘∅) ≺ 𝐴 ↔ ∅ ≺ 𝐴)
27	24, 26	syl6ibr 251	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
28	1, 2, 27	3syl 18	. . . . . . . . . 10 ⊢ (𝐴 ∈ Inacc → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
29		eloni 6276	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → Ord 𝐴)
30		ordtr 6280	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝐴 → Tr 𝐴)
31	29, 30	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ On → Tr 𝐴)
32		trsuc 6350	. . . . . . . . . . . . . . 15 ⊢ ((Tr 𝐴 ∧ suc 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
33	32	ex 413	. . . . . . . . . . . . . 14 ⊢ (Tr 𝐴 → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
34	3, 31, 33	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Inacc → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
35	34	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
36		r1suc 9528	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) = 𝒫 (𝑅1‘𝑦))
37		fvex 6787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅1‘𝑦) ∈ V
38	37	cardid 10303	. . . . . . . . . . . . . . . . 17 ⊢ (card‘(𝑅1‘𝑦)) ≈ (𝑅1‘𝑦)
39	38	ensymi 8790	. . . . . . . . . . . . . . . 16 ⊢ (𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦))
40		pwen 8937	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦)) → 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦))
42	36, 41	eqbrtrdi 5113	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
43		winacard 10448	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
44	43	eleq2d 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
45		cardsdom 10311	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅1‘𝑦) ∈ V ∧ 𝐴 ∈ On) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
46	37, 2, 45	sylancr 587	. . . . . . . . . . . . . . . . . 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 10443	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴))
50	49	simp3bi 1146	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inacc → ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴)
51		pweq 4549	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → 𝒫 𝑧 = 𝒫 (card‘(𝑅1‘𝑦)))
52	51	breq1d 5084	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → (𝒫 𝑧 ≺ 𝐴 ↔ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
53	52	rspccv 3558	. . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Inacc ∧ (𝑅1‘𝑦) ≺ 𝐴) → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴)
57		ensdomtr 8900	. . . . . . . . . . . . . 14 ⊢ (((𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)) ∧ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴) → (𝑅1‘suc 𝑦) ≺ 𝐴)
58	42, 56, 57	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ On ∧ (𝐴 ∈ Inacc ∧ (𝑅1‘𝑦) ≺ 𝐴)) → (𝑅1‘suc 𝑦) ≺ 𝐴)
59	58	expr 457	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑅1‘𝑦) ≺ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))
60	35, 59	imim12d 81	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
61	60	ex 413	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (𝐴 ∈ Inacc → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))))
62		vex 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
63		r1lim 9530	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
64	62, 63	mpan 687	. . . . . . . . . . . . . . 15 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
65		nfcv 2907	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝑧
66		nfcv 2907	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑅1‘𝑧)
67		nfcv 2907	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦 ≼
68		nfiu1 4958	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
69	66, 67, 68	nfbr 5121	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦(𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
70		fveq2 6774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑧 → (𝑅1‘𝑦) = (𝑅1‘𝑧))
71	70	breq1d 5084	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → ((𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
72		fvex 6787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (card‘(𝑅1‘𝑦)) ∈ V
73	62, 72	iunex 7811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ V
74		ssiun2 4977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
75		ssdomg 8786	. . . . . . . . . . . . . . . . . . . . 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 8798	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦)) ∧ (card‘(𝑅1‘𝑦)) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
78	39, 76, 77	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
79	65, 69, 71, 78	vtoclgaf 3512	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑥 → (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
80	79	rgen 3074	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
81		iundom 10298	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
82	62, 80, 81	mp2an 689	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
83	62, 73	unex 7596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V
84		ssun2 4107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
85		ssdomg 8786	. . . . . . . . . . . . . . . . . . . 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 8854	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
88	86, 87	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
89		ssun1 4106	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
90		ssdomg 8786	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
91	83, 89, 90	mp2 9	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
92	83	xpdom1 8858	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
94		domtr 8793	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ∧ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
95	88, 93, 94	mp2an 689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
96		limomss 7717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑥 → ω ⊆ 𝑥)
97	96, 89	sstrdi 3933	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝑥 → ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
98		ssdomg 8786	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
99	83, 97, 98	mpsyl 68	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑥 → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
100		infxpidm 10318	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
101	99, 100	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑥 → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
102		domentr 8799	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ∧ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
103	95, 101, 102	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (Lim 𝑥 → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
104		domtr 8793	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∧ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
105	82, 103, 104	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (Lim 𝑥 → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
106	64, 105	eqbrtrd 5096	. . . . . . . . . . . . . 14 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
107	106	ad2antlr 724	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
108		eleq1a 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 → (𝐴 = 𝑥 → 𝐴 ∈ 𝐴))
109		ordirr 6284	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)
110	3, 29, 109	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Inacc → ¬ 𝐴 ∈ 𝐴)
111	108, 110	nsyli 157	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → (𝐴 ∈ Inacc → ¬ 𝐴 = 𝑥))
112	111	imp 407	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ Inacc) → ¬ 𝐴 = 𝑥)
113	112	ad2ant2r 744	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = 𝑥)
114		simpll 764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ 𝐴)
115		limord 6325	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Lim 𝑥 → Ord 𝑥)
116	62	elon 6275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ Ord 𝑥)
117	115, 116	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑥 → 𝑥 ∈ On)
118	117	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ On)
119		cardf 10306	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ card:V⟶On
120		r1fnon 9525	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑅1 Fn On
121		dffn2 6602	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅1 Fn On ↔ 𝑅1:On⟶V)
122	120, 121	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅1:On⟶V
123		fco 6624	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((card:V⟶On ∧ 𝑅1:On⟶V) → (card ∘ 𝑅1):On⟶On)
124	119, 122, 123	mp2an 689	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (card ∘ 𝑅1):On⟶On
125		onss 7634	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
126		fssres 6640	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((card ∘ 𝑅1):On⟶On ∧ 𝑥 ⊆ On) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
127	124, 125, 126	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
128		ffn 6600	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
129	118, 127, 128	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
130	3	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On)
131		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
132		simplll 772	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝐴)
133		ontr1 6312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
134	133	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ On ∧ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) → 𝑦 ∈ 𝐴)
135	130, 131, 132, 134	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
136	37, 130, 45	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
137	1, 43	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐴 ∈ Inacc → (card‘𝐴) = 𝐴)
138	137	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (card‘𝐴) = 𝐴)
139	138	eleq2d 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → 𝑥 ∈ On)
144		fvres 6793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ 𝑥 → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
145	144	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
146		onelon 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
147		fvco3 6867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅1:On⟶V ∧ 𝑦 ∈ On) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
148	122, 146, 147	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
149	145, 148	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1‘𝑦)))
150	143, 149	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1‘𝑦)))
151	150	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴 ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
152	142, 151	sylibrd 258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
153	152	ralimdva 3108	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
154	153	impr 455	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴)
155		ffnfv 6992	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ↔ (((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
156	129, 154, 155	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴)
157		eleq2 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
158	157	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
159		eliun 4928	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ ∃𝑦 ∈ 𝑥 𝑧 ∈ (card‘(𝑅1‘𝑦)))
160		cardon 9702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (card‘(𝑅1‘𝑦)) ∈ On
161	160	onelssi 6375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (card‘(𝑅1‘𝑦)))
162	149	sseq2d 3953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ↔ 𝑧 ⊆ (card‘(𝑅1‘𝑦))))
163	161, 162	syl5ibr 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
164	163	reximdva 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 𝑧 ∈ (card‘(𝑅1‘𝑦)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
165	159, 164	syl5bi 241	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ On → (𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
166	158, 165	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On → ((𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
167	166	expdimp 453	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
168	167	ralrimiv 3102	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
169	168	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
170	118, 169	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
171		ffun 6603	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((card ∘ 𝑅1):On⟶On → Fun (card ∘ 𝑅1))
172	124, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (card ∘ 𝑅1)
173		resfunexg 7091	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (card ∘ 𝑅1) ∧ 𝑥 ∈ V) → ((card ∘ 𝑅1) ↾ 𝑥) ∈ V)
174	172, 62, 173	mp2an 689	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((card ∘ 𝑅1) ↾ 𝑥) ∈ V
175		feq1 6581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤:𝑥⟶𝐴 ↔ ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴))
176		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤‘𝑦) = (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
177	176	sseq2d 3953	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑧 ⊆ (𝑤‘𝑦) ↔ 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
178	177	rexbidv 3226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
179	178	ralbidv 3112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
180	175, 179	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → ((𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) ↔ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))))
181	174, 180	spcev 3545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)))
182	156, 170, 181	syl6an 681	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦))))
183	3	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝐴 ∈ On)
184		cfflb 10015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
185	183, 118, 184	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
186	182, 185	syld 47	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
187	49	simp2bi 1145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ Inacc → (cf‘𝐴) = 𝐴)
188	187	sseq1d 3952	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ Inacc → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
189	188	ad2antrl 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
190	186, 189	sylibd 238	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → 𝐴 ⊆ 𝑥))
191		ontri1 6300	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴))
192	183, 118, 191	syl2anc 584	. . . . . . . . . . . . . . . . . 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 8170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
196	62, 195	mpan 687	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
197	160	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ∈ On)
198	196, 197	mprg 3078	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On
199		eqcom 2745	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 ↔ 𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
200		eloni 6276	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → Ord 𝑥)
201		eloni 6276	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → Ord ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
202		ordequn 6366	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord 𝑥 ∧ Ord ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
203	200, 201, 202	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → (𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
204	199, 203	syl5bi 241	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
205	118, 198, 204	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
206	113, 194, 205	mtord 877	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)
207		onelss 6308	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
208	183, 114, 207	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ⊆ 𝐴)
209		onelss 6308	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∈ On → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
210	130, 142, 209	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
211	210	ralimdva 3108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
212	211	impr 455	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
213		iunss 4975	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
214	212, 213	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
215	208, 214	unssd 4120	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴)
216		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → 𝑥 = if(𝑥 ∈ On, 𝑥, ∅))
217		iuneq1 4940	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) = ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)))
218	216, 217	uneq12d 4098	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))))
219	218	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On ↔ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))) ∈ On))
220		0elon 6319	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∅ ∈ On
221	220	elimel 4528	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ On
222	221	elexi 3451	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ V
223		iunon 8170	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((if(𝑥 ∈ On, 𝑥, ∅) ∈ V ∧ ∀𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On)
224	222, 223	mpan 687	. . . . . . . . . . . . . . . . . . . . . . . 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 3078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On
227	221, 226	onun2i 6382	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))) ∈ On
228	219, 227	dedth 4517	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
229	117, 228	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑥 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
230	229	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ Lim 𝑥) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
231	3	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)) → 𝐴 ∈ On)
232		onsseleq 6307	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On ∧ 𝐴 ∈ On) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴 ↔ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)))
233	230, 231, 232	syl2an 596	. . . . . . . . . . . . . . . . . 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 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 725	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (card‘𝐴) = 𝐴)
239		iscard 9733	. . . . . . . . . . . . . . . 16 ⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴))
240	239	simprbi 497	. . . . . . . . . . . . . . 15 ⊢ ((card‘𝐴) = 𝐴 → ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴)
241		breq1 5077	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑧 ≺ 𝐴 ↔ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴))
242	241	rspccv 3558	. . . . . . . . . . . . . . 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 8899	. . . . . . . . . . . . 13 ⊢ (((𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∧ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
246	107, 244, 245	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑅1‘𝑥) ≺ 𝐴)
247	246	exp43 437	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴))))
248	247	com4l 92	. . . . . . . . . 10 ⊢ (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴))))
249	13, 17, 21, 28, 61, 248	tfinds2 7710	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (𝐴 ∈ Inacc → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴)))
250	249	impd 411	. . . . . . . 8 ⊢ (𝑥 ∈ On → ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴))
251	9, 250	mpcom 38	. . . . . . 7 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
252		sdomdom 8768	. . . . . . 7 ⊢ ((𝑅1‘𝑥) ≺ 𝐴 → (𝑅1‘𝑥) ≼ 𝐴)
253	251, 252	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≼ 𝐴)
254	253	ralrimiva 3103	. . . . 5 ⊢ (𝐴 ∈ Inacc → ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴)
255		iundom 10298	. . . . 5 ⊢ ((𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴) → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
256	3, 254, 255	syl2anc 584	. . . 4 ⊢ (𝐴 ∈ Inacc → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
257	7, 256	eqbrtrd 5096	. . 3 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ (𝐴 × 𝐴))
258		winainf 10450	. . . . 5 ⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
259	1, 258	syl 17	. . . 4 ⊢ (𝐴 ∈ Inacc → ω ⊆ 𝐴)
260		infxpen 9770	. . . 4 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
261	3, 259, 260	syl2anc 584	. . 3 ⊢ (𝐴 ∈ Inacc → (𝐴 × 𝐴) ≈ 𝐴)
262		domentr 8799	. . 3 ⊢ (((𝑅1‘𝐴) ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≈ 𝐴) → (𝑅1‘𝐴) ≼ 𝐴)
263	257, 261, 262	syl2anc 584	. 2 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ 𝐴)
264		fvex 6787	. . 3 ⊢ (𝑅1‘𝐴) ∈ V
265	122	fdmi 6612	. . . . 5 ⊢ dom 𝑅1 = On
266	2, 265	eleqtrrdi 2850	. . . 4 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ dom 𝑅1)
267		onssr1 9589	. . . 4 ⊢ (𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴))
268	1, 266, 267	3syl 18	. . 3 ⊢ (𝐴 ∈ Inacc → 𝐴 ⊆ (𝑅1‘𝐴))
269		ssdomg 8786	. . 3 ⊢ ((𝑅1‘𝐴) ∈ V → (𝐴 ⊆ (𝑅1‘𝐴) → 𝐴 ≼ (𝑅1‘𝐴)))
270	264, 268, 269	mpsyl 68	. 2 ⊢ (𝐴 ∈ Inacc → 𝐴 ≼ (𝑅1‘𝐴))
271		sbth 8880	. 2 ⊢ (((𝑅1‘𝐴) ≼ 𝐴 ∧ 𝐴 ≼ (𝑅1‘𝐴)) → (𝑅1‘𝐴) ≈ 𝐴)
272	263, 270, 271	syl2anc 584	1 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∪ cun 3885   ⊆ wss 3887  ∅c0 4256  ifcif 4459  𝒫 cpw 4533  ∪ ciun 4924   class class class wbr 5074  Tr wtr 5191   × cxp 5587  dom cdm 5589   ↾ cres 5591   ∘ ccom 5593  Ord word 6265  Oncon0 6266  Lim wlim 6267  suc csuc 6268  Fun wfun 6427   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433  ωcom 7712   ≈ cen 8730   ≼ cdom 8731   ≺ csdm 8732  𝑅₁cr1 9520  cardccrd 9693  cfccf 9695  Inacc_wcwina 10438  Inacccina 10439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-ac2 10219

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-oi 9269  df-r1 9522  df-rank 9523  df-card 9697  df-cf 9699  df-acn 9700  df-ac 9872  df-wina 10440  df-ina 10441

This theorem is referenced by:  r1omALT  10532  inatsk  10534