Theorem inar1 10462

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 10377	. . . . . 6 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
2		winaon 10375	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On)
3	1, 2	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ On)
4		winalim 10382	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → Lim 𝐴)
5	1, 4	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → Lim 𝐴)
6		r1lim 9461	. . . . 5 ⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
7	3, 5, 6	syl2anc 583	. . . 4 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
8		onelon 6276	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
9	3, 8	sylan 579	. . . . . . . 8 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
10		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
11		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑅1‘𝑥) = (𝑅1‘∅))
12	11	breq1d 5080	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘∅) ≺ 𝐴))
13	10, 12	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴)))
14		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
15		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
16	15	breq1d 5080	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
17	14, 16	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)))
18		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴))
19		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
20	19	breq1d 5080	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘suc 𝑦) ≺ 𝐴))
21	18, 20	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
22		ne0i 4265	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝐴 → 𝐴 ≠ ∅)
23		0sdomg 8842	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ On → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
24	22, 23	syl5ibr 245	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ≺ 𝐴))
25		r10 9457	. . . . . . . . . . . . 13 ⊢ (𝑅1‘∅) = ∅
26	25	breq1i 5077	. . . . . . . . . . . 12 ⊢ ((𝑅1‘∅) ≺ 𝐴 ↔ ∅ ≺ 𝐴)
27	24, 26	syl6ibr 251	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
28	1, 2, 27	3syl 18	. . . . . . . . . 10 ⊢ (𝐴 ∈ Inacc → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
29		eloni 6261	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → Ord 𝐴)
30		ordtr 6265	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝐴 → Tr 𝐴)
31	29, 30	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ On → Tr 𝐴)
32		trsuc 6335	. . . . . . . . . . . . . . 15 ⊢ ((Tr 𝐴 ∧ suc 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
33	32	ex 412	. . . . . . . . . . . . . 14 ⊢ (Tr 𝐴 → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
34	3, 31, 33	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Inacc → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
35	34	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴))
36		r1suc 9459	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) = 𝒫 (𝑅1‘𝑦))
37		fvex 6769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅1‘𝑦) ∈ V
38	37	cardid 10234	. . . . . . . . . . . . . . . . 17 ⊢ (card‘(𝑅1‘𝑦)) ≈ (𝑅1‘𝑦)
39	38	ensymi 8745	. . . . . . . . . . . . . . . 16 ⊢ (𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦))
40		pwen 8886	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦)) → 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦))
42	36, 41	eqbrtrdi 5109	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
43		winacard 10379	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
44	43	eleq2d 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
45		cardsdom 10242	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅1‘𝑦) ∈ V ∧ 𝐴 ∈ On) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
46	37, 2, 45	sylancr 586	. . . . . . . . . . . . . . . . . 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 10374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴))
50	49	simp3bi 1145	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inacc → ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴)
51		pweq 4546	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → 𝒫 𝑧 = 𝒫 (card‘(𝑅1‘𝑦)))
52	51	breq1d 5080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → (𝒫 𝑧 ≺ 𝐴 ↔ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
53	52	rspccv 3549	. . . . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Inacc ∧ (𝑅1‘𝑦) ≺ 𝐴) → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴)
57		ensdomtr 8849	. . . . . . . . . . . . . 14 ⊢ (((𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)) ∧ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴) → (𝑅1‘suc 𝑦) ≺ 𝐴)
58	42, 56, 57	syl2an 595	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ On ∧ (𝐴 ∈ Inacc ∧ (𝑅1‘𝑦) ≺ 𝐴)) → (𝑅1‘suc 𝑦) ≺ 𝐴)
59	58	expr 456	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑅1‘𝑦) ≺ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))
60	35, 59	imim12d 81	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
61	60	ex 412	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (𝐴 ∈ Inacc → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))))
62		vex 3426	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
63		r1lim 9461	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
64	62, 63	mpan 686	. . . . . . . . . . . . . . 15 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
65		nfcv 2906	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝑧
66		nfcv 2906	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑅1‘𝑧)
67		nfcv 2906	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦 ≼
68		nfiu1 4955	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
69	66, 67, 68	nfbr 5117	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦(𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
70		fveq2 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑧 → (𝑅1‘𝑦) = (𝑅1‘𝑧))
71	70	breq1d 5080	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → ((𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
72		fvex 6769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (card‘(𝑅1‘𝑦)) ∈ V
73	62, 72	iunex 7784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ V
74		ssiun2 4973	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
75		ssdomg 8741	. . . . . . . . . . . . . . . . . . . . 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 8753	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦)) ∧ (card‘(𝑅1‘𝑦)) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
78	39, 76, 77	sylancr 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
79	65, 69, 71, 78	vtoclgaf 3502	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑥 → (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
80	79	rgen 3073	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
81		iundom 10229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
82	62, 80, 81	mp2an 688	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
83	62, 73	unex 7574	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V
84		ssun2 4103	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
85		ssdomg 8741	. . . . . . . . . . . . . . . . . . . 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 8807	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
88	86, 87	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
89		ssun1 4102	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
90		ssdomg 8741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
91	83, 89, 90	mp2 9	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
92	83	xpdom1 8811	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
94		domtr 8748	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ∧ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
95	88, 93, 94	mp2an 688	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
96		limomss 7692	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑥 → ω ⊆ 𝑥)
97	96, 89	sstrdi 3929	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝑥 → ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
98		ssdomg 8741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
99	83, 97, 98	mpsyl 68	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑥 → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
100		infxpidm 10249	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
101	99, 100	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑥 → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
102		domentr 8754	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ∧ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
103	95, 101, 102	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ (Lim 𝑥 → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
104		domtr 8748	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∧ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
105	82, 103, 104	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ (Lim 𝑥 → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
106	64, 105	eqbrtrd 5092	. . . . . . . . . . . . . 14 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
107	106	ad2antlr 723	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
108		eleq1a 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 → (𝐴 = 𝑥 → 𝐴 ∈ 𝐴))
109		ordirr 6269	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)
110	3, 29, 109	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Inacc → ¬ 𝐴 ∈ 𝐴)
111	108, 110	nsyli 157	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → (𝐴 ∈ Inacc → ¬ 𝐴 = 𝑥))
112	111	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ Inacc) → ¬ 𝐴 = 𝑥)
113	112	ad2ant2r 743	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = 𝑥)
114		simpll 763	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ 𝐴)
115		limord 6310	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Lim 𝑥 → Ord 𝑥)
116	62	elon 6260	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ Ord 𝑥)
117	115, 116	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑥 → 𝑥 ∈ On)
118	117	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ On)
119		cardf 10237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ card:V⟶On
120		r1fnon 9456	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑅1 Fn On
121		dffn2 6586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅1 Fn On ↔ 𝑅1:On⟶V)
122	120, 121	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅1:On⟶V
123		fco 6608	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((card:V⟶On ∧ 𝑅1:On⟶V) → (card ∘ 𝑅1):On⟶On)
124	119, 122, 123	mp2an 688	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (card ∘ 𝑅1):On⟶On
125		onss 7611	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
126		fssres 6624	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((card ∘ 𝑅1):On⟶On ∧ 𝑥 ⊆ On) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
127	124, 125, 126	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
128		ffn 6584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
129	118, 127, 128	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
130	3	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On)
131		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
132		simplll 771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝐴)
133		ontr1 6297	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
134	133	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ On ∧ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) → 𝑦 ∈ 𝐴)
135	130, 131, 132, 134	syl12anc 833	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
136	37, 130, 45	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
137	1, 43	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐴 ∈ Inacc → (card‘𝐴) = 𝐴)
138	137	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → 𝑥 ∈ On)
144		fvres 6775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ 𝑥 → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
145	144	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
146		onelon 6276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
147		fvco3 6849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅1:On⟶V ∧ 𝑦 ∈ On) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
148	122, 146, 147	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
149	145, 148	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1‘𝑦)))
150	143, 149	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3102	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
154	153	impr 454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴)
155		ffnfv 6974	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ↔ (((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
156	129, 154, 155	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴)
157		eleq2 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
158	157	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
159		eliun 4925	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ ∃𝑦 ∈ 𝑥 𝑧 ∈ (card‘(𝑅1‘𝑦)))
160		cardon 9633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (card‘(𝑅1‘𝑦)) ∈ On
161	160	onelssi 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (card‘(𝑅1‘𝑦)))
162	149	sseq2d 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ↔ 𝑧 ⊆ (card‘(𝑅1‘𝑦))))
163	161, 162	syl5ibr 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
164	163	reximdva 3202	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 452	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
168	167	ralrimiv 3106	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
169	168	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
170	118, 169	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
171		ffun 6587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((card ∘ 𝑅1):On⟶On → Fun (card ∘ 𝑅1))
172	124, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (card ∘ 𝑅1)
173		resfunexg 7073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (card ∘ 𝑅1) ∧ 𝑥 ∈ V) → ((card ∘ 𝑅1) ↾ 𝑥) ∈ V)
174	172, 62, 173	mp2an 688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((card ∘ 𝑅1) ↾ 𝑥) ∈ V
175		feq1 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤:𝑥⟶𝐴 ↔ ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴))
176		fveq1 6755	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤‘𝑦) = (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
177	176	sseq2d 3949	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑧 ⊆ (𝑤‘𝑦) ↔ 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
178	177	rexbidv 3225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
179	178	ralbidv 3120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
180	175, 179	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → ((𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) ↔ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))))
181	174, 180	spcev 3535	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)))
182	156, 170, 181	syl6an 680	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦))))
183	3	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝐴 ∈ On)
184		cfflb 9946	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
185	183, 118, 184	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
186	182, 185	syld 47	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
187	49	simp2bi 1144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ Inacc → (cf‘𝐴) = 𝐴)
188	187	sseq1d 3948	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ Inacc → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
189	188	ad2antrl 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
190	186, 189	sylibd 238	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → 𝐴 ⊆ 𝑥))
191		ontri1 6285	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴))
192	183, 118, 191	syl2anc 583	. . . . . . . . . . . . . . . . . 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 8141	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
196	62, 195	mpan 686	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
197	160	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ∈ On)
198	196, 197	mprg 3077	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On
199		eqcom 2745	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 ↔ 𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
200		eloni 6261	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → Ord 𝑥)
201		eloni 6261	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → Ord ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
202		ordequn 6351	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord 𝑥 ∧ Ord ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
203	200, 201, 202	syl2an 595	. . . . . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
206	113, 194, 205	mtord 876	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)
207		onelss 6293	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
208	183, 114, 207	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ⊆ 𝐴)
209		onelss 6293	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∈ On → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
210	130, 142, 209	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
211	210	ralimdva 3102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
212	211	impr 454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
213		iunss 4971	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
214	212, 213	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
215	208, 214	unssd 4116	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴)
216		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → 𝑥 = if(𝑥 ∈ On, 𝑥, ∅))
217		iuneq1 4937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) = ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)))
218	216, 217	uneq12d 4094	. . . . . . . . . . . . . . . . . . . . . . 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 6304	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∅ ∈ On
221	220	elimel 4525	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ On
222	221	elexi 3441	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ V
223		iunon 8141	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((if(𝑥 ∈ On, 𝑥, ∅) ∈ V ∧ ∀𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On)
224	222, 223	mpan 686	. . . . . . . . . . . . . . . . . . . . . . . 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 3077	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On
227	221, 226	onun2i 6367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))) ∈ On
228	219, 227	dedth 4514	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
229	117, 228	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑥 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
230	229	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ Lim 𝑥) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On)
231	3	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)) → 𝐴 ∈ On)
232		onsseleq 6292	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On ∧ 𝐴 ∈ On) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴 ↔ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)))
233	230, 231, 232	syl2an 595	. . . . . . . . . . . . . . . . . 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 867	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴))
236	235	ord 860	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (¬ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴))
237	206, 236	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴)
238	137	ad2antrl 724	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (card‘𝐴) = 𝐴)
239		iscard 9664	. . . . . . . . . . . . . . . 16 ⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴))
240	239	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ ((card‘𝐴) = 𝐴 → ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴)
241		breq1 5073	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑧 ≺ 𝐴 ↔ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴))
242	241	rspccv 3549	. . . . . . . . . . . . . . 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 8848	. . . . . . . . . . . . 13 ⊢ (((𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∧ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
246	107, 244, 245	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑅1‘𝑥) ≺ 𝐴)
247	246	exp43 436	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴))))
248	247	com4l 92	. . . . . . . . . 10 ⊢ (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴))))
249	13, 17, 21, 28, 61, 248	tfinds2 7685	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (𝐴 ∈ Inacc → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴)))
250	249	impd 410	. . . . . . . 8 ⊢ (𝑥 ∈ On → ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴))
251	9, 250	mpcom 38	. . . . . . 7 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
252		sdomdom 8723	. . . . . . 7 ⊢ ((𝑅1‘𝑥) ≺ 𝐴 → (𝑅1‘𝑥) ≼ 𝐴)
253	251, 252	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≼ 𝐴)
254	253	ralrimiva 3107	. . . . 5 ⊢ (𝐴 ∈ Inacc → ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴)
255		iundom 10229	. . . . 5 ⊢ ((𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴) → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
256	3, 254, 255	syl2anc 583	. . . 4 ⊢ (𝐴 ∈ Inacc → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
257	7, 256	eqbrtrd 5092	. . 3 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ (𝐴 × 𝐴))
258		winainf 10381	. . . . 5 ⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
259	1, 258	syl 17	. . . 4 ⊢ (𝐴 ∈ Inacc → ω ⊆ 𝐴)
260		infxpen 9701	. . . 4 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
261	3, 259, 260	syl2anc 583	. . 3 ⊢ (𝐴 ∈ Inacc → (𝐴 × 𝐴) ≈ 𝐴)
262		domentr 8754	. . 3 ⊢ (((𝑅1‘𝐴) ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≈ 𝐴) → (𝑅1‘𝐴) ≼ 𝐴)
263	257, 261, 262	syl2anc 583	. 2 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ 𝐴)
264		fvex 6769	. . 3 ⊢ (𝑅1‘𝐴) ∈ V
265	122	fdmi 6596	. . . . 5 ⊢ dom 𝑅1 = On
266	2, 265	eleqtrrdi 2850	. . . 4 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ dom 𝑅1)
267		onssr1 9520	. . . 4 ⊢ (𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴))
268	1, 266, 267	3syl 18	. . 3 ⊢ (𝐴 ∈ Inacc → 𝐴 ⊆ (𝑅1‘𝐴))
269		ssdomg 8741	. . 3 ⊢ ((𝑅1‘𝐴) ∈ V → (𝐴 ⊆ (𝑅1‘𝐴) → 𝐴 ≼ (𝑅1‘𝐴)))
270	264, 268, 269	mpsyl 68	. 2 ⊢ (𝐴 ∈ Inacc → 𝐴 ≼ (𝑅1‘𝐴))
271		sbth 8833	. 2 ⊢ (((𝑅1‘𝐴) ≼ 𝐴 ∧ 𝐴 ≼ (𝑅1‘𝐴)) → (𝑅1‘𝐴) ≈ 𝐴)
272	263, 270, 271	syl2anc 583	1 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  Vcvv 3422   ∪ cun 3881   ⊆ wss 3883  ∅c0 4253  ifcif 4456  𝒫 cpw 4530  ∪ ciun 4921   class class class wbr 5070  Tr wtr 5187   × cxp 5578  dom cdm 5580   ↾ cres 5582   ∘ ccom 5584  Ord word 6250  Oncon0 6251  Lim wlim 6252  suc csuc 6253  Fun wfun 6412   Fn wfn 6413  ⟶wf 6414  ‘cfv 6418  ωcom 7687   ≈ cen 8688   ≼ cdom 8689   ≺ csdm 8690  𝑅₁cr1 9451  cardccrd 9624  cfccf 9626  Inacc_wcwina 10369  Inacccina 10370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329  ax-ac2 10150

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-2o 8268  df-er 8456  df-map 8575  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-oi 9199  df-r1 9453  df-rank 9454  df-card 9628  df-cf 9630  df-acn 9631  df-ac 9803  df-wina 10371  df-ina 10372

This theorem is referenced by:  r1omALT  10463  inatsk  10465