Theorem inar1 10728

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 10643	. . . . . 6 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
2		winaon 10641	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On)
3	1, 2	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ On)
4		winalim 10648	. . . . . 6 ⊢ (𝐴 ∈ Inaccw → Lim 𝐴)
5	1, 4	syl 17	. . . . 5 ⊢ (𝐴 ∈ Inacc → Lim 𝐴)
6		r1lim 9725	. . . . 5 ⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
7	3, 5, 6	syl2anc 584	. . . 4 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
8		onelon 6357	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
9	3, 8	sylan 580	. . . . . . . 8 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On)
10		eleq1 2816	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
11		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑅1‘𝑥) = (𝑅1‘∅))
12	11	breq1d 5117	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘∅) ≺ 𝐴))
13	10, 12	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴)))
14		eleq1 2816	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
15		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
16	15	breq1d 5117	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
17	14, 16	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)))
18		eleq1 2816	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴))
19		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
20	19	breq1d 5117	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘suc 𝑦) ≺ 𝐴))
21	18, 20	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
22		ne0i 4304	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝐴 → 𝐴 ≠ ∅)
23		0sdomg 9070	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ On → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
24	22, 23	imbitrrid 246	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ≺ 𝐴))
25		r10 9721	. . . . . . . . . . . . 13 ⊢ (𝑅1‘∅) = ∅
26	25	breq1i 5114	. . . . . . . . . . . 12 ⊢ ((𝑅1‘∅) ≺ 𝐴 ↔ ∅ ≺ 𝐴)
27	24, 26	imbitrrdi 252	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
28	1, 2, 27	3syl 18	. . . . . . . . . 10 ⊢ (𝐴 ∈ Inacc → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
29		eloni 6342	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → Ord 𝐴)
30		ordtr 6346	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝐴 → Tr 𝐴)
31	29, 30	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ On → Tr 𝐴)
32		trsuc 6421	. . . . . . . . . . . . . . 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 9723	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) = 𝒫 (𝑅1‘𝑦))
37		fvex 6871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅1‘𝑦) ∈ V
38	37	cardid 10500	. . . . . . . . . . . . . . . . 17 ⊢ (card‘(𝑅1‘𝑦)) ≈ (𝑅1‘𝑦)
39	38	ensymi 8975	. . . . . . . . . . . . . . . 16 ⊢ (𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦))
40		pwen 9114	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅1‘𝑦) ≈ (card‘(𝑅1‘𝑦)) → 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 𝒫 (𝑅1‘𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦))
42	36, 41	eqbrtrdi 5146	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ On → (𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)))
43		winacard 10645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
44	43	eleq2d 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
45		cardsdom 10508	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅1‘𝑦) ∈ V ∧ 𝐴 ∈ On) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
46	37, 2, 45	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴))
47	44, 46	bitr3d 281	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inaccw → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
48	1, 47	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Inacc → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴))
49		elina 10640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴))
50	49	simp3bi 1147	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inacc → ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴)
51		pweq 4577	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → 𝒫 𝑧 = 𝒫 (card‘(𝑅1‘𝑦)))
52	51	breq1d 5117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (card‘(𝑅1‘𝑦)) → (𝒫 𝑧 ≺ 𝐴 ↔ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
53	52	rspccv 3585	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴 → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
54	50, 53	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Inacc → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
55	48, 54	sylbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Inacc → ((𝑅1‘𝑦) ≺ 𝐴 → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴))
56	55	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Inacc ∧ (𝑅1‘𝑦) ≺ 𝐴) → 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴)
57		ensdomtr 9077	. . . . . . . . . . . . . 14 ⊢ (((𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1‘𝑦)) ∧ 𝒫 (card‘(𝑅1‘𝑦)) ≺ 𝐴) → (𝑅1‘suc 𝑦) ≺ 𝐴)
58	42, 56, 57	syl2an 596	. . . . . . . . . . . . 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 3451	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
63		r1lim 9725	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
64	62, 63	mpan 690	. . . . . . . . . . . . . . 15 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧))
65		nfcv 2891	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝑧
66		nfcv 2891	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑅1‘𝑧)
67		nfcv 2891	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦 ≼
68		nfiu1 4991	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
69	66, 67, 68	nfbr 5154	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦(𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
70		fveq2 6858	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑧 → (𝑅1‘𝑦) = (𝑅1‘𝑧))
71	70	breq1d 5117	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → ((𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
72		fvex 6871	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (card‘(𝑅1‘𝑦)) ∈ V
73	62, 72	iunex 7947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ V
74		ssiun2 5011	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
75		ssdomg 8971	. . . . . . . . . . . . . . . . . . . . 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 8983	. . . . . . . . . . . . . . . . . . . 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 3542	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑥 → (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
80	79	rgen 3046	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))
81		iundom 10495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
82	62, 80, 81	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
83	62, 73	unex 7720	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V
84		ssun2 4142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
85		ssdomg 8971	. . . . . . . . . . . . . . . . . . . 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 9036	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
88	86, 87	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
89		ssun1 4141	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
90		ssdomg 8971	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (𝑥 ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
91	83, 89, 90	mp2 9	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
92	83	xpdom1 9040	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
94		domtr 8978	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ∧ (𝑥 × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))) → (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
95	88, 93, 94	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
96		limomss 7847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑥 → ω ⊆ 𝑥)
97	96, 89	sstrdi 3959	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝑥 → ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
98		ssdomg 8971	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ V → (ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))))
99	83, 97, 98	mpsyl 68	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑥 → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
100		infxpidm 10515	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
101	99, 100	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑥 → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
102		domentr 8984	. . . . . . . . . . . . . . . . 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 8978	. . . . . . . . . . . . . . . 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 5129	. . . . . . . . . . . . . 14 ⊢ (Lim 𝑥 → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
107	106	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
108		eleq1a 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 → (𝐴 = 𝑥 → 𝐴 ∈ 𝐴))
109		ordirr 6350	. . . . . . . . . . . . . . . . . . . 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 747	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = 𝑥)
114		simpll 766	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ 𝐴)
115		limord 6393	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Lim 𝑥 → Ord 𝑥)
116	62	elon 6341	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ Ord 𝑥)
117	115, 116	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑥 → 𝑥 ∈ On)
118	117	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ On)
119		cardf 10503	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ card:V⟶On
120		r1fnon 9720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑅1 Fn On
121		dffn2 6690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅1 Fn On ↔ 𝑅1:On⟶V)
122	120, 121	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅1:On⟶V
123		fco 6712	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((card:V⟶On ∧ 𝑅1:On⟶V) → (card ∘ 𝑅1):On⟶On)
124	119, 122, 123	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (card ∘ 𝑅1):On⟶On
125		onss 7761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
126		fssres 6726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((card ∘ 𝑅1):On⟶On ∧ 𝑥 ⊆ On) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
127	124, 125, 126	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
128		ffn 6688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
129	118, 127, 128	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
130	3	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On)
131		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
132		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝐴)
133		ontr1 6379	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
134	133	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ On ∧ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) → 𝑦 ∈ 𝐴)
135	130, 131, 132, 134	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (card‘𝐴) = 𝐴)
139	138	eleq2d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
140	136, 139	bitr3d 281	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑦) ≺ 𝐴 ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
141	140	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑦) ≺ 𝐴 → (card‘(𝑅1‘𝑦)) ∈ 𝐴))
142	135, 141	embantd 59	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (card‘(𝑅1‘𝑦)) ∈ 𝐴))
143	117	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → 𝑥 ∈ On)
144		fvres 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ 𝑥 → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
145	144	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
146		onelon 6357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
147		fvco3 6960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1‘𝑦)))
150	143, 149	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1‘𝑦)))
151	150	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴 ↔ (card‘(𝑅1‘𝑦)) ∈ 𝐴))
152	142, 151	sylibrd 259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
153	152	ralimdva 3145	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
154	153	impr 454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴)
155		ffnfv 7091	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ↔ (((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
156	129, 154, 155	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴)
157		eleq2 2817	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
158	157	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
159		eliun 4959	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ↔ ∃𝑦 ∈ 𝑥 𝑧 ∈ (card‘(𝑅1‘𝑦)))
160		cardon 9897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (card‘(𝑅1‘𝑦)) ∈ On
161	160	onelssi 6449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (card‘(𝑅1‘𝑦)))
162	149	sseq2d 3979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ↔ 𝑧 ⊆ (card‘(𝑅1‘𝑦))))
163	161, 162	imbitrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ∈ (card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
164	163	reximdva 3146	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 𝑧 ∈ (card‘(𝑅1‘𝑦)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
165	159, 164	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3124	. . . . . . . . . . . . . . . . . . . . . . 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 6691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((card ∘ 𝑅1):On⟶On → Fun (card ∘ 𝑅1))
172	124, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (card ∘ 𝑅1)
173		resfunexg 7189	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (card ∘ 𝑅1) ∧ 𝑥 ∈ V) → ((card ∘ 𝑅1) ↾ 𝑥) ∈ V)
174	172, 62, 173	mp2an 692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((card ∘ 𝑅1) ↾ 𝑥) ∈ V
175		feq1 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤:𝑥⟶𝐴 ↔ ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴))
176		fveq1 6857	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤‘𝑦) = (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
177	176	sseq2d 3979	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑧 ⊆ (𝑤‘𝑦) ↔ 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
178	177	rexbidv 3157	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
179	178	ralbidv 3156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
180	175, 179	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → ((𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) ↔ (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))))
181	174, 180	spcev 3572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)))
182	156, 170, 181	syl6an 684	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦))))
183	3	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝐴 ∈ On)
184		cfflb 10212	. . . . . . . . . . . . . . . . . . . . 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 1146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ Inacc → (cf‘𝐴) = 𝐴)
188	187	sseq1d 3978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ Inacc → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
189	188	ad2antrl 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
190	186, 189	sylibd 239	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → 𝐴 ⊆ 𝑥))
191		ontri1 6366	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴))
192	183, 118, 191	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴))
193	190, 192	sylibd 239	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) → ¬ 𝑥 ∈ 𝐴))
194	114, 193	mt2d 136	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
195		iunon 8308	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
196	62, 195	mpan 690	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On)
197	160	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑥 → (card‘(𝑅1‘𝑦)) ∈ On)
198	196, 197	mprg 3050	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On
199		eqcom 2736	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 ↔ 𝐴 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))))
200		eloni 6342	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → Ord 𝑥)
201		eloni 6342	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ∈ On → Ord ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)))
202		ordequn 6437	. . . . . . . . . . . . . . . . . . 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	biimtrid 242	. . . . . . . . . . . . . . . . 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 879	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴)
207		onelss 6374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
208	183, 114, 207	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ⊆ 𝐴)
209		onelss 6374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∈ On → ((card‘(𝑅1‘𝑦)) ∈ 𝐴 → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
210	130, 142, 209	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
211	210	ralimdva 3145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴))
212	211	impr 454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
213		iunss 5009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
214	212, 213	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) ⊆ 𝐴)
215	208, 214	unssd 4155	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ⊆ 𝐴)
216		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → 𝑥 = if(𝑥 ∈ On, 𝑥, ∅))
217		iuneq1 4972	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦)) = ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)))
218	216, 217	uneq12d 4132	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))))
219	218	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ On ↔ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))) ∈ On))
220		0elon 6387	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∅ ∈ On
221	220	elimel 4558	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ On
222	221	elexi 3470	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ V
223		iunon 8308	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((if(𝑥 ∈ On, 𝑥, ∅) ∈ V ∧ ∀𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On)
224	222, 223	mpan 690	. . . . . . . . . . . . . . . . . . . . . . . 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 3050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦)) ∈ On
227	221, 226	onun2i 6456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1‘𝑦))) ∈ On
228	219, 227	dedth 4547	. . . . . . . . . . . . . . . . . . . . 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 6373	. . . . . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴))
235	234	orcomd 871	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 ∨ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴))
236	235	ord 864	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (¬ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) = 𝐴 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴))
237	206, 236	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∈ 𝐴)
238	137	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (card‘𝐴) = 𝐴)
239		iscard 9928	. . . . . . . . . . . . . . . 16 ⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴))
240	239	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ ((card‘𝐴) = 𝐴 → ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴)
241		breq1 5110	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) → (𝑧 ≺ 𝐴 ↔ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴))
242	241	rspccv 3585	. . . . . . . . . . . . . . 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 9076	. . . . . . . . . . . . 13 ⊢ (((𝑅1‘𝑥) ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ∧ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥 (card‘(𝑅1‘𝑦))) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
246	107, 244, 245	syl2anc 584	. . . . . . . . . . . 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 7840	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (𝐴 ∈ Inacc → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴)))
250	249	impd 410	. . . . . . . 8 ⊢ (𝑥 ∈ On → ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴))
251	9, 250	mpcom 38	. . . . . . 7 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)
252		sdomdom 8951	. . . . . . 7 ⊢ ((𝑅1‘𝑥) ≺ 𝐴 → (𝑅1‘𝑥) ≼ 𝐴)
253	251, 252	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≼ 𝐴)
254	253	ralrimiva 3125	. . . . 5 ⊢ (𝐴 ∈ Inacc → ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴)
255		iundom 10495	. . . . 5 ⊢ ((𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴) → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
256	3, 254, 255	syl2anc 584	. . . 4 ⊢ (𝐴 ∈ Inacc → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴))
257	7, 256	eqbrtrd 5129	. . 3 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ (𝐴 × 𝐴))
258		winainf 10647	. . . . 5 ⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
259	1, 258	syl 17	. . . 4 ⊢ (𝐴 ∈ Inacc → ω ⊆ 𝐴)
260		infxpen 9967	. . . 4 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
261	3, 259, 260	syl2anc 584	. . 3 ⊢ (𝐴 ∈ Inacc → (𝐴 × 𝐴) ≈ 𝐴)
262		domentr 8984	. . 3 ⊢ (((𝑅1‘𝐴) ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≈ 𝐴) → (𝑅1‘𝐴) ≼ 𝐴)
263	257, 261, 262	syl2anc 584	. 2 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≼ 𝐴)
264		fvex 6871	. . 3 ⊢ (𝑅1‘𝐴) ∈ V
265	122	fdmi 6699	. . . . 5 ⊢ dom 𝑅1 = On
266	2, 265	eleqtrrdi 2839	. . . 4 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ dom 𝑅1)
267		onssr1 9784	. . . 4 ⊢ (𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴))
268	1, 266, 267	3syl 18	. . 3 ⊢ (𝐴 ∈ Inacc → 𝐴 ⊆ (𝑅1‘𝐴))
269		ssdomg 8971	. . 3 ⊢ ((𝑅1‘𝐴) ∈ V → (𝐴 ⊆ (𝑅1‘𝐴) → 𝐴 ≼ (𝑅1‘𝐴)))
270	264, 268, 269	mpsyl 68	. 2 ⊢ (𝐴 ∈ Inacc → 𝐴 ≼ (𝑅1‘𝐴))
271		sbth 9061	. 2 ⊢ (((𝑅1‘𝐴) ≼ 𝐴 ∧ 𝐴 ≼ (𝑅1‘𝐴)) → (𝑅1‘𝐴) ≈ 𝐴)
272	263, 270, 271	syl2anc 584	1 ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  Vcvv 3447   ∪ cun 3912   ⊆ wss 3914  ∅c0 4296  ifcif 4488  𝒫 cpw 4563  ∪ ciun 4955   class class class wbr 5107  Tr wtr 5214   × cxp 5636  dom cdm 5638   ↾ cres 5640   ∘ ccom 5642  Ord word 6331  Oncon0 6332  Lim wlim 6333  suc csuc 6334  Fun wfun 6505   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511  ωcom 7842   ≈ cen 8915   ≼ cdom 8916   ≺ csdm 8917  𝑅₁cr1 9715  cardccrd 9888  cfccf 9890  Inacc_wcwina 10635  Inacccina 10636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594  ax-ac2 10416

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-2o 8435  df-er 8671  df-map 8801  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-oi 9463  df-r1 9717  df-rank 9718  df-card 9892  df-cf 9894  df-acn 9895  df-ac 10069  df-wina 10637  df-ina 10638

This theorem is referenced by:  r1omALT  10729  inatsk  10731