inar1

Description: ( R1A ) for A a strongly inaccessible cardinal is equipotent to A . (Contributed by Mario Carneiro, 6-Jun-2013)

		Ref	Expression
	Assertion	inar1	$⊢ A \in Inacc \to R_{1} (A) \approx A$

Proof

Step	Hyp	Ref	Expression
1		inawina	$⊢ A \in Inacc \to A \in {Inacc}_{𝑤}$
2		winaon	$⊢ A \in {Inacc}_{𝑤} \to A \in On$
3	1 2	syl	$⊢ A \in Inacc \to A \in On$
4		winalim	$⊢ A \in {Inacc}_{𝑤} \to Lim A$
5	1 4	syl	$⊢ A \in Inacc \to Lim A$
6		r1lim	$⊢ (A \in On \land Lim A) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$
7	3 5 6	syl2anc	$⊢ A \in Inacc \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$
8		onelon	$⊢ (A \in On \land x \in A) \to x \in On$
9	3 8	sylan	$⊢ (A \in Inacc \land x \in A) \to x \in On$
10		eleq1	$⊢ x = \emptyset \to (x \in A \leftrightarrow \emptyset \in A)$
11		fveq2	$⊢ x = \emptyset \to R_{1} (x) = R_{1} (\emptyset)$
12	11	breq1d	$⊢ x = \emptyset \to (R_{1} (x) ≺ A \leftrightarrow R_{1} (\emptyset) ≺ A)$
13	10 12	imbi12d	$⊢ x = \emptyset \to ((x \in A \to R_{1} (x) ≺ A) \leftrightarrow (\emptyset \in A \to R_{1} (\emptyset) ≺ A))$
14		eleq1	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
15		fveq2	$⊢ x = y \to R_{1} (x) = R_{1} (y)$
16	15	breq1d	$⊢ x = y \to (R_{1} (x) ≺ A \leftrightarrow R_{1} (y) ≺ A)$
17	14 16	imbi12d	$⊢ x = y \to ((x \in A \to R_{1} (x) ≺ A) \leftrightarrow (y \in A \to R_{1} (y) ≺ A))$
18		eleq1	$⊢ x = suc y \to (x \in A \leftrightarrow suc y \in A)$
19		fveq2	$⊢ x = suc y \to R_{1} (x) = R_{1} (suc y)$
20	19	breq1d	$⊢ x = suc y \to (R_{1} (x) ≺ A \leftrightarrow R_{1} (suc y) ≺ A)$
21	18 20	imbi12d	$⊢ x = suc y \to ((x \in A \to R_{1} (x) ≺ A) \leftrightarrow (suc y \in A \to R_{1} (suc y) ≺ A))$
22		ne0i	$⊢ \emptyset \in A \to A \neq \emptyset$
23		0sdomg	$⊢ A \in On \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
24	22 23	imbitrrid	$⊢ A \in On \to (\emptyset \in A \to \emptyset ≺ A)$
25		r10	$⊢ R_{1} (\emptyset) = \emptyset$
26	25	breq1i	$⊢ R_{1} (\emptyset) ≺ A \leftrightarrow \emptyset ≺ A$
27	24 26	imbitrrdi	$⊢ A \in On \to (\emptyset \in A \to R_{1} (\emptyset) ≺ A)$
28	1 2 27	3syl	$⊢ A \in Inacc \to (\emptyset \in A \to R_{1} (\emptyset) ≺ A)$
29		eloni	$⊢ A \in On \to Ord A$
30		ordtr	$⊢ Ord A \to Tr A$
31	29 30	syl	$⊢ A \in On \to Tr A$
32		trsuc	$⊢ (Tr A \land suc y \in A) \to y \in A$
33	32	ex	$⊢ Tr A \to (suc y \in A \to y \in A)$
34	3 31 33	3syl	$⊢ A \in Inacc \to (suc y \in A \to y \in A)$
35	34	adantl	$⊢ (y \in On \land A \in Inacc) \to (suc y \in A \to y \in A)$
36		r1suc	$⊢ y \in On \to R_{1} (suc y) = 𝒫 R_{1} (y)$
37		fvex	$⊢ R_{1} (y) \in V$
38	37	cardid	$⊢ card (R_{1} (y)) \approx R_{1} (y)$
39	38	ensymi	$⊢ R_{1} (y) \approx card (R_{1} (y))$
40		pwen	$⊢ R_{1} (y) \approx card (R_{1} (y)) \to 𝒫 R_{1} (y) \approx 𝒫 card (R_{1} (y))$
41	39 40	ax-mp	$⊢ 𝒫 R_{1} (y) \approx 𝒫 card (R_{1} (y))$
42	36 41	eqbrtrdi	$⊢ y \in On \to R_{1} (suc y) \approx 𝒫 card (R_{1} (y))$
43		winacard	$⊢ A \in {Inacc}_{𝑤} \to card (A) = A$
44	43	eleq2d	$⊢ A \in {Inacc}_{𝑤} \to (card (R_{1} (y)) \in card (A) \leftrightarrow card (R_{1} (y)) \in A)$
45		cardsdom	$⊢ (R_{1} (y) \in V \land A \in On) \to (card (R_{1} (y)) \in card (A) \leftrightarrow R_{1} (y) ≺ A)$
46	37 2 45	sylancr	$⊢ A \in {Inacc}_{𝑤} \to (card (R_{1} (y)) \in card (A) \leftrightarrow R_{1} (y) ≺ A)$
47	44 46	bitr3d	$⊢ A \in {Inacc}_{𝑤} \to (card (R_{1} (y)) \in A \leftrightarrow R_{1} (y) ≺ A)$
48	1 47	syl	$⊢ A \in Inacc \to (card (R_{1} (y)) \in A \leftrightarrow R_{1} (y) ≺ A)$
49		elina	$⊢ A \in Inacc \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall z \in A 𝒫 z ≺ A)$
50	49	simp3bi	$⊢ A \in Inacc \to \forall z \in A 𝒫 z ≺ A$
51		pweq	$⊢ z = card (R_{1} (y)) \to 𝒫 z = 𝒫 card (R_{1} (y))$
52	51	breq1d	$⊢ z = card (R_{1} (y)) \to (𝒫 z ≺ A \leftrightarrow 𝒫 card (R_{1} (y)) ≺ A)$
53	52	rspccv	$⊢ \forall z \in A 𝒫 z ≺ A \to (card (R_{1} (y)) \in A \to 𝒫 card (R_{1} (y)) ≺ A)$
54	50 53	syl	$⊢ A \in Inacc \to (card (R_{1} (y)) \in A \to 𝒫 card (R_{1} (y)) ≺ A)$
55	48 54	sylbird	$⊢ A \in Inacc \to (R_{1} (y) ≺ A \to 𝒫 card (R_{1} (y)) ≺ A)$
56	55	imp	$⊢ (A \in Inacc \land R_{1} (y) ≺ A) \to 𝒫 card (R_{1} (y)) ≺ A$
57		ensdomtr	$⊢ (R_{1} (suc y) \approx 𝒫 card (R_{1} (y)) \land 𝒫 card (R_{1} (y)) ≺ A) \to R_{1} (suc y) ≺ A$
58	42 56 57	syl2an	$⊢ (y \in On \land (A \in Inacc \land R_{1} (y) ≺ A)) \to R_{1} (suc y) ≺ A$
59	58	expr	$⊢ (y \in On \land A \in Inacc) \to (R_{1} (y) ≺ A \to R_{1} (suc y) ≺ A)$
60	35 59	imim12d	$⊢ (y \in On \land A \in Inacc) \to ((y \in A \to R_{1} (y) ≺ A) \to (suc y \in A \to R_{1} (suc y) ≺ A))$
61	60	ex	$⊢ y \in On \to (A \in Inacc \to ((y \in A \to R_{1} (y) ≺ A) \to (suc y \in A \to R_{1} (suc y) ≺ A)))$
62		vex	$⊢ x \in V$
63		r1lim	$⊢ (x \in V \land Lim x) \to R_{1} (x) = ⋃_{z \in x} R_{1} (z)$
64	62 63	mpan	$⊢ Lim x \to R_{1} (x) = ⋃_{z \in x} R_{1} (z)$
65		nfcv	$⊢ \underline{Ⅎ} y z$
66		nfcv	$⊢ \underline{Ⅎ} y R_{1} (z)$
67		nfcv	$⊢ \underline{Ⅎ} y ≼$
68		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in x} card (R_{1} (y))$
69	66 67 68	nfbr	$⊢ Ⅎ y R_{1} (z) ≼ ⋃_{y \in x} card (R_{1} (y))$
70		fveq2	$⊢ y = z \to R_{1} (y) = R_{1} (z)$
71	70	breq1d	$⊢ y = z \to (R_{1} (y) ≼ ⋃_{y \in x} card (R_{1} (y)) \leftrightarrow R_{1} (z) ≼ ⋃_{y \in x} card (R_{1} (y)))$
72		fvex	$⊢ card (R_{1} (y)) \in V$
73	62 72	iunex	$⊢ ⋃_{y \in x} card (R_{1} (y)) \in V$
74		ssiun2	$⊢ y \in x \to card (R_{1} (y)) \subseteq ⋃_{y \in x} card (R_{1} (y))$
75		ssdomg	$⊢ ⋃_{y \in x} card (R_{1} (y)) \in V \to (card (R_{1} (y)) \subseteq ⋃_{y \in x} card (R_{1} (y)) \to card (R_{1} (y)) ≼ ⋃_{y \in x} card (R_{1} (y)))$
76	73 74 75	mpsyl	$⊢ y \in x \to card (R_{1} (y)) ≼ ⋃_{y \in x} card (R_{1} (y))$
77		endomtr	$⊢ (R_{1} (y) \approx card (R_{1} (y)) \land card (R_{1} (y)) ≼ ⋃_{y \in x} card (R_{1} (y))) \to R_{1} (y) ≼ ⋃_{y \in x} card (R_{1} (y))$
78	39 76 77	sylancr	$⊢ y \in x \to R_{1} (y) ≼ ⋃_{y \in x} card (R_{1} (y))$
79	65 69 71 78	vtoclgaf	$⊢ z \in x \to R_{1} (z) ≼ ⋃_{y \in x} card (R_{1} (y))$
80	79	rgen	$⊢ \forall z \in x R_{1} (z) ≼ ⋃_{y \in x} card (R_{1} (y))$
81		iundom	$⊢ (x \in V \land \forall z \in x R_{1} (z) ≼ ⋃_{y \in x} card (R_{1} (y))) \to ⋃_{z \in x} R_{1} (z) ≼ (x \times ⋃_{y \in x} card (R_{1} (y)))$
82	62 80 81	mp2an	$⊢ ⋃_{z \in x} R_{1} (z) ≼ (x \times ⋃_{y \in x} card (R_{1} (y)))$
83	62 73	unex	$⊢ x \cup ⋃_{y \in x} card (R_{1} (y)) \in V$
84		ssun2	$⊢ ⋃_{y \in x} card (R_{1} (y)) \subseteq x \cup ⋃_{y \in x} card (R_{1} (y))$
85		ssdomg	$⊢ x \cup ⋃_{y \in x} card (R_{1} (y)) \in V \to (⋃_{y \in x} card (R_{1} (y)) \subseteq x \cup ⋃_{y \in x} card (R_{1} (y)) \to ⋃_{y \in x} card (R_{1} (y)) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y))))$
86	83 84 85	mp2	$⊢ ⋃_{y \in x} card (R_{1} (y)) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))$
87	62	xpdom2	$⊢ ⋃_{y \in x} card (R_{1} (y)) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y))) \to (x \times ⋃_{y \in x} card (R_{1} (y))) ≼ (x \times (x \cup ⋃_{y \in x} card (R_{1} (y))))$
88	86 87	ax-mp	$⊢ (x \times ⋃_{y \in x} card (R_{1} (y))) ≼ (x \times (x \cup ⋃_{y \in x} card (R_{1} (y))))$
89		ssun1	$⊢ x \subseteq x \cup ⋃_{y \in x} card (R_{1} (y))$
90		ssdomg	$⊢ x \cup ⋃_{y \in x} card (R_{1} (y)) \in V \to (x \subseteq x \cup ⋃_{y \in x} card (R_{1} (y)) \to x ≼ (x \cup ⋃_{y \in x} card (R_{1} (y))))$
91	83 89 90	mp2	$⊢ x ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))$
92	83	xpdom1	$⊢ x ≼ (x \cup ⋃_{y \in x} card (R_{1} (y))) \to (x \times (x \cup ⋃_{y \in x} card (R_{1} (y)))) ≼ ((x \cup ⋃_{y \in x} card (R_{1} (y))) \times (x \cup ⋃_{y \in x} card (R_{1} (y))))$
93	91 92	ax-mp	$⊢ (x \times (x \cup ⋃_{y \in x} card (R_{1} (y)))) ≼ ((x \cup ⋃_{y \in x} card (R_{1} (y))) \times (x \cup ⋃_{y \in x} card (R_{1} (y))))$
94		domtr	$⊢ ((x \times ⋃_{y \in x} card (R_{1} (y))) ≼ (x \times (x \cup ⋃_{y \in x} card (R_{1} (y)))) \land (x \times (x \cup ⋃_{y \in x} card (R_{1} (y)))) ≼ ((x \cup ⋃_{y \in x} card (R_{1} (y))) \times (x \cup ⋃_{y \in x} card (R_{1} (y))))) \to (x \times ⋃_{y \in x} card (R_{1} (y))) ≼ ((x \cup ⋃_{y \in x} card (R_{1} (y))) \times (x \cup ⋃_{y \in x} card (R_{1} (y))))$
95	88 93 94	mp2an	$⊢ (x \times ⋃_{y \in x} card (R_{1} (y))) ≼ ((x \cup ⋃_{y \in x} card (R_{1} (y))) \times (x \cup ⋃_{y \in x} card (R_{1} (y))))$
96		limomss	$⊢ Lim x \to ω \subseteq x$
97	96 89	sstrdi	$⊢ Lim x \to ω \subseteq x \cup ⋃_{y \in x} card (R_{1} (y))$
98		ssdomg	$⊢ x \cup ⋃_{y \in x} card (R_{1} (y)) \in V \to (ω \subseteq x \cup ⋃_{y \in x} card (R_{1} (y)) \to ω ≼ (x \cup ⋃_{y \in x} card (R_{1} (y))))$
99	83 97 98	mpsyl	$⊢ Lim x \to ω ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))$
100		infxpidm	$⊢ ω ≼ (x \cup ⋃_{y \in x} card (R_{1} (y))) \to ((x \cup ⋃_{y \in x} card (R_{1} (y))) \times (x \cup ⋃_{y \in x} card (R_{1} (y)))) \approx (x \cup ⋃_{y \in x} card (R_{1} (y)))$
101	99 100	syl	$⊢ Lim x \to ((x \cup ⋃_{y \in x} card (R_{1} (y))) \times (x \cup ⋃_{y \in x} card (R_{1} (y)))) \approx (x \cup ⋃_{y \in x} card (R_{1} (y)))$
102		domentr	$⊢ ((x \times ⋃_{y \in x} card (R_{1} (y))) ≼ ((x \cup ⋃_{y \in x} card (R_{1} (y))) \times (x \cup ⋃_{y \in x} card (R_{1} (y)))) \land ((x \cup ⋃_{y \in x} card (R_{1} (y))) \times (x \cup ⋃_{y \in x} card (R_{1} (y)))) \approx (x \cup ⋃_{y \in x} card (R_{1} (y)))) \to (x \times ⋃_{y \in x} card (R_{1} (y))) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))$
103	95 101 102	sylancr	$⊢ Lim x \to (x \times ⋃_{y \in x} card (R_{1} (y))) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))$
104		domtr	$⊢ (⋃_{z \in x} R_{1} (z) ≼ (x \times ⋃_{y \in x} card (R_{1} (y))) \land (x \times ⋃_{y \in x} card (R_{1} (y))) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))) \to ⋃_{z \in x} R_{1} (z) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))$
105	82 103 104	sylancr	$⊢ Lim x \to ⋃_{z \in x} R_{1} (z) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))$
106	64 105	eqbrtrd	$⊢ Lim x \to R_{1} (x) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))$
107	106	ad2antlr	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to R_{1} (x) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y)))$
108		eleq1a	$⊢ x \in A \to (A = x \to A \in A)$
109		ordirr	$⊢ Ord A \to \neg A \in A$
110	3 29 109	3syl	$⊢ A \in Inacc \to \neg A \in A$
111	108 110	nsyli	$⊢ x \in A \to (A \in Inacc \to \neg A = x)$
112	111	imp	$⊢ (x \in A \land A \in Inacc) \to \neg A = x$
113	112	ad2ant2r	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to \neg A = x$
114		simpll	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to x \in A$
115		limord	$⊢ Lim x \to Ord x$
116	62	elon	$⊢ x \in On \leftrightarrow Ord x$
117	115 116	sylibr	$⊢ Lim x \to x \in On$
118	117	ad2antlr	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to x \in On$
119		cardf	$⊢ card : V ⟶ On$
120		r1fnon	$⊢ R_{1} Fn On$
121		dffn2	$⊢ R_{1} Fn On \leftrightarrow R_{1} : On ⟶ V$
122	120 121	mpbi	$⊢ R_{1} : On ⟶ V$
123		fco	$⊢ (card : V ⟶ On \land R_{1} : On ⟶ V) \to (card \circ R_{1}) : On ⟶ On$
124	119 122 123	mp2an	$⊢ (card \circ R_{1}) : On ⟶ On$
125		onss	$⊢ x \in On \to x \subseteq On$
126		fssres	$⊢ ((card \circ R_{1}) : On ⟶ On \land x \subseteq On) \to ({(card \circ R_{1}) ↾}_{x}) : x ⟶ On$
127	124 125 126	sylancr	$⊢ x \in On \to ({(card \circ R_{1}) ↾}_{x}) : x ⟶ On$
128		ffn	$⊢ ({(card \circ R_{1}) ↾}_{x}) : x ⟶ On \to ({(card \circ R_{1}) ↾}_{x}) Fn x$
129	118 127 128	3syl	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to ({(card \circ R_{1}) ↾}_{x}) Fn x$
130	3	ad2antlr	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to A \in On$
131		simpr	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to y \in x$
132		simplll	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to x \in A$
133		ontr1	$⊢ A \in On \to ((y \in x \land x \in A) \to y \in A)$
134	133	imp	$⊢ (A \in On \land (y \in x \land x \in A)) \to y \in A$
135	130 131 132 134	syl12anc	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to y \in A$
136	37 130 45	sylancr	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to (card (R_{1} (y)) \in card (A) \leftrightarrow R_{1} (y) ≺ A)$
137	1 43	syl	$⊢ A \in Inacc \to card (A) = A$
138	137	ad2antlr	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to card (A) = A$
139	138	eleq2d	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to (card (R_{1} (y)) \in card (A) \leftrightarrow card (R_{1} (y)) \in A)$
140	136 139	bitr3d	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to (R_{1} (y) ≺ A \leftrightarrow card (R_{1} (y)) \in A)$
141	140	biimpd	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to (R_{1} (y) ≺ A \to card (R_{1} (y)) \in A)$
142	135 141	embantd	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to ((y \in A \to R_{1} (y) ≺ A) \to card (R_{1} (y)) \in A)$
143	117	ad2antlr	$⊢ ((x \in A \land Lim x) \land A \in Inacc) \to x \in On$
144		fvres	$⊢ y \in x \to ({(card \circ R_{1}) ↾}_{x}) (y) = (card \circ R_{1}) (y)$
145	144	adantl	$⊢ (x \in On \land y \in x) \to ({(card \circ R_{1}) ↾}_{x}) (y) = (card \circ R_{1}) (y)$
146		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
147		fvco3	$⊢ (R_{1} : On ⟶ V \land y \in On) \to (card \circ R_{1}) (y) = card (R_{1} (y))$
148	122 146 147	sylancr	$⊢ (x \in On \land y \in x) \to (card \circ R_{1}) (y) = card (R_{1} (y))$
149	145 148	eqtrd	$⊢ (x \in On \land y \in x) \to ({(card \circ R_{1}) ↾}_{x}) (y) = card (R_{1} (y))$
150	143 149	sylan	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to ({(card \circ R_{1}) ↾}_{x}) (y) = card (R_{1} (y))$
151	150	eleq1d	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to (({(card \circ R_{1}) ↾}_{x}) (y) \in A \leftrightarrow card (R_{1} (y)) \in A)$
152	142 151	sylibrd	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to ((y \in A \to R_{1} (y) ≺ A) \to ({(card \circ R_{1}) ↾}_{x}) (y) \in A)$
153	152	ralimdva	$⊢ ((x \in A \land Lim x) \land A \in Inacc) \to (\forall y \in x (y \in A \to R_{1} (y) ≺ A) \to \forall y \in x ({(card \circ R_{1}) ↾}_{x}) (y) \in A)$
154	153	impr	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to \forall y \in x ({(card \circ R_{1}) ↾}_{x}) (y) \in A$
155		ffnfv	$⊢ ({(card \circ R_{1}) ↾}_{x}) : x ⟶ A \leftrightarrow (({(card \circ R_{1}) ↾}_{x}) Fn x \land \forall y \in x ({(card \circ R_{1}) ↾}_{x}) (y) \in A)$
156	129 154 155	sylanbrc	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to ({(card \circ R_{1}) ↾}_{x}) : x ⟶ A$
157		eleq2	$⊢ A = ⋃_{y \in x} card (R_{1} (y)) \to (z \in A \leftrightarrow z \in ⋃_{y \in x} card (R_{1} (y)))$
158	157	biimpa	$⊢ (A = ⋃_{y \in x} card (R_{1} (y)) \land z \in A) \to z \in ⋃_{y \in x} card (R_{1} (y))$
159		eliun	$⊢ z \in ⋃_{y \in x} card (R_{1} (y)) \leftrightarrow \exists y \in x z \in card (R_{1} (y))$
160		cardon	$⊢ card (R_{1} (y)) \in On$
161	160	onelssi	$⊢ z \in card (R_{1} (y)) \to z \subseteq card (R_{1} (y))$
162	149	sseq2d	$⊢ (x \in On \land y \in x) \to (z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y) \leftrightarrow z \subseteq card (R_{1} (y)))$
163	161 162	imbitrrid	$⊢ (x \in On \land y \in x) \to (z \in card (R_{1} (y)) \to z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
164	163	reximdva	$⊢ x \in On \to (\exists y \in x z \in card (R_{1} (y)) \to \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
165	159 164	biimtrid	$⊢ x \in On \to (z \in ⋃_{y \in x} card (R_{1} (y)) \to \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
166	158 165	syl5	$⊢ x \in On \to ((A = ⋃_{y \in x} card (R_{1} (y)) \land z \in A) \to \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
167	166	expdimp	$⊢ (x \in On \land A = ⋃_{y \in x} card (R_{1} (y))) \to (z \in A \to \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
168	167	ralrimiv	$⊢ (x \in On \land A = ⋃_{y \in x} card (R_{1} (y))) \to \forall z \in A \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y)$
169	168	ex	$⊢ x \in On \to (A = ⋃_{y \in x} card (R_{1} (y)) \to \forall z \in A \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
170	118 169	syl	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (A = ⋃_{y \in x} card (R_{1} (y)) \to \forall z \in A \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
171		ffun	$⊢ (card \circ R_{1}) : On ⟶ On \to Fun (card \circ R_{1})$
172	124 171	ax-mp	$⊢ Fun (card \circ R_{1})$
173		resfunexg	$⊢ (Fun (card \circ R_{1}) \land x \in V) \to {(card \circ R_{1}) ↾}_{x} \in V$
174	172 62 173	mp2an	$⊢ {(card \circ R_{1}) ↾}_{x} \in V$
175		feq1	$⊢ w = {(card \circ R_{1}) ↾}_{x} \to (w : x ⟶ A \leftrightarrow ({(card \circ R_{1}) ↾}_{x}) : x ⟶ A)$
176		fveq1	$⊢ w = {(card \circ R_{1}) ↾}_{x} \to w (y) = ({(card \circ R_{1}) ↾}_{x}) (y)$
177	176	sseq2d	$⊢ w = {(card \circ R_{1}) ↾}_{x} \to (z \subseteq w (y) \leftrightarrow z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
178	177	rexbidv	$⊢ w = {(card \circ R_{1}) ↾}_{x} \to (\exists y \in x z \subseteq w (y) \leftrightarrow \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
179	178	ralbidv	$⊢ w = {(card \circ R_{1}) ↾}_{x} \to (\forall z \in A \exists y \in x z \subseteq w (y) \leftrightarrow \forall z \in A \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y))$
180	175 179	anbi12d	$⊢ w = {(card \circ R_{1}) ↾}_{x} \to ((w : x ⟶ A \land \forall z \in A \exists y \in x z \subseteq w (y)) \leftrightarrow (({(card \circ R_{1}) ↾}_{x}) : x ⟶ A \land \forall z \in A \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y)))$
181	174 180	spcev	$⊢ (({(card \circ R_{1}) ↾}_{x}) : x ⟶ A \land \forall z \in A \exists y \in x z \subseteq ({(card \circ R_{1}) ↾}_{x}) (y)) \to \exists w (w : x ⟶ A \land \forall z \in A \exists y \in x z \subseteq w (y))$
182	156 170 181	syl6an	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (A = ⋃_{y \in x} card (R_{1} (y)) \to \exists w (w : x ⟶ A \land \forall z \in A \exists y \in x z \subseteq w (y)))$
183	3	ad2antrl	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to A \in On$
184		cfflb	$⊢ (A \in On \land x \in On) \to (\exists w (w : x ⟶ A \land \forall z \in A \exists y \in x z \subseteq w (y)) \to cf (A) \subseteq x)$
185	183 118 184	syl2anc	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (\exists w (w : x ⟶ A \land \forall z \in A \exists y \in x z \subseteq w (y)) \to cf (A) \subseteq x)$
186	182 185	syld	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (A = ⋃_{y \in x} card (R_{1} (y)) \to cf (A) \subseteq x)$
187	49	simp2bi	$⊢ A \in Inacc \to cf (A) = A$
188	187	sseq1d	$⊢ A \in Inacc \to (cf (A) \subseteq x \leftrightarrow A \subseteq x)$
189	188	ad2antrl	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (cf (A) \subseteq x \leftrightarrow A \subseteq x)$
190	186 189	sylibd	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (A = ⋃_{y \in x} card (R_{1} (y)) \to A \subseteq x)$
191		ontri1	$⊢ (A \in On \land x \in On) \to (A \subseteq x \leftrightarrow \neg x \in A)$
192	183 118 191	syl2anc	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (A \subseteq x \leftrightarrow \neg x \in A)$
193	190 192	sylibd	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (A = ⋃_{y \in x} card (R_{1} (y)) \to \neg x \in A)$
194	114 193	mt2d	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to \neg A = ⋃_{y \in x} card (R_{1} (y))$
195		iunon	$⊢ (x \in V \land \forall y \in x card (R_{1} (y)) \in On) \to ⋃_{y \in x} card (R_{1} (y)) \in On$
196	62 195	mpan	$⊢ \forall y \in x card (R_{1} (y)) \in On \to ⋃_{y \in x} card (R_{1} (y)) \in On$
197	160	a1i	$⊢ y \in x \to card (R_{1} (y)) \in On$
198	196 197	mprg	$⊢ ⋃_{y \in x} card (R_{1} (y)) \in On$
199		eqcom	$⊢ x \cup ⋃_{y \in x} card (R_{1} (y)) = A \leftrightarrow A = x \cup ⋃_{y \in x} card (R_{1} (y))$
200		eloni	$⊢ x \in On \to Ord x$
201		eloni	$⊢ ⋃_{y \in x} card (R_{1} (y)) \in On \to Ord ⋃_{y \in x} card (R_{1} (y))$
202		ordequn	$⊢ (Ord x \land Ord ⋃_{y \in x} card (R_{1} (y))) \to (A = x \cup ⋃_{y \in x} card (R_{1} (y)) \to (A = x \lor A = ⋃_{y \in x} card (R_{1} (y))))$
203	200 201 202	syl2an	$⊢ (x \in On \land ⋃_{y \in x} card (R_{1} (y)) \in On) \to (A = x \cup ⋃_{y \in x} card (R_{1} (y)) \to (A = x \lor A = ⋃_{y \in x} card (R_{1} (y))))$
204	199 203	biimtrid	$⊢ (x \in On \land ⋃_{y \in x} card (R_{1} (y)) \in On) \to (x \cup ⋃_{y \in x} card (R_{1} (y)) = A \to (A = x \lor A = ⋃_{y \in x} card (R_{1} (y))))$
205	118 198 204	sylancl	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (x \cup ⋃_{y \in x} card (R_{1} (y)) = A \to (A = x \lor A = ⋃_{y \in x} card (R_{1} (y))))$
206	113 194 205	mtord	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to \neg x \cup ⋃_{y \in x} card (R_{1} (y)) = A$
207		onelss	$⊢ A \in On \to (x \in A \to x \subseteq A)$
208	183 114 207	sylc	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to x \subseteq A$
209		onelss	$⊢ A \in On \to (card (R_{1} (y)) \in A \to card (R_{1} (y)) \subseteq A)$
210	130 142 209	sylsyld	$⊢ (((x \in A \land Lim x) \land A \in Inacc) \land y \in x) \to ((y \in A \to R_{1} (y) ≺ A) \to card (R_{1} (y)) \subseteq A)$
211	210	ralimdva	$⊢ ((x \in A \land Lim x) \land A \in Inacc) \to (\forall y \in x (y \in A \to R_{1} (y) ≺ A) \to \forall y \in x card (R_{1} (y)) \subseteq A)$
212	211	impr	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to \forall y \in x card (R_{1} (y)) \subseteq A$
213		iunss	$⊢ ⋃_{y \in x} card (R_{1} (y)) \subseteq A \leftrightarrow \forall y \in x card (R_{1} (y)) \subseteq A$
214	212 213	sylibr	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to ⋃_{y \in x} card (R_{1} (y)) \subseteq A$
215	208 214	unssd	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to x \cup ⋃_{y \in x} card (R_{1} (y)) \subseteq A$
216		id	$⊢ x = if (x \in On, x, \emptyset) \to x = if (x \in On, x, \emptyset)$
217		iuneq1	$⊢ x = if (x \in On, x, \emptyset) \to ⋃_{y \in x} card (R_{1} (y)) = ⋃_{y \in if (x \in On, x, \emptyset)} card (R_{1} (y))$
218	216 217	uneq12d	$⊢ x = if (x \in On, x, \emptyset) \to x \cup ⋃_{y \in x} card (R_{1} (y)) = if (x \in On, x, \emptyset) \cup ⋃_{y \in if (x \in On, x, \emptyset)} card (R_{1} (y))$
219	218	eleq1d	$⊢ x = if (x \in On, x, \emptyset) \to (x \cup ⋃_{y \in x} card (R_{1} (y)) \in On \leftrightarrow if (x \in On, x, \emptyset) \cup ⋃_{y \in if (x \in On, x, \emptyset)} card (R_{1} (y)) \in On)$
220		0elon	$⊢ \emptyset \in On$
221	220	elimel	$⊢ if (x \in On, x, \emptyset) \in On$
222	221	elexi	$⊢ if (x \in On, x, \emptyset) \in V$
223		iunon	$⊢ (if (x \in On, x, \emptyset) \in V \land \forall y \in if (x \in On, x, \emptyset) card (R_{1} (y)) \in On) \to ⋃_{y \in if (x \in On, x, \emptyset)} card (R_{1} (y)) \in On$
224	222 223	mpan	$⊢ \forall y \in if (x \in On, x, \emptyset) card (R_{1} (y)) \in On \to ⋃_{y \in if (x \in On, x, \emptyset)} card (R_{1} (y)) \in On$
225	160	a1i	$⊢ y \in if (x \in On, x, \emptyset) \to card (R_{1} (y)) \in On$
226	224 225	mprg	$⊢ ⋃_{y \in if (x \in On, x, \emptyset)} card (R_{1} (y)) \in On$
227	221 226	onun2i	$⊢ if (x \in On, x, \emptyset) \cup ⋃_{y \in if (x \in On, x, \emptyset)} card (R_{1} (y)) \in On$
228	219 227	dedth	$⊢ x \in On \to x \cup ⋃_{y \in x} card (R_{1} (y)) \in On$
229	117 228	syl	$⊢ Lim x \to x \cup ⋃_{y \in x} card (R_{1} (y)) \in On$
230	229	adantl	$⊢ (x \in A \land Lim x) \to x \cup ⋃_{y \in x} card (R_{1} (y)) \in On$
231	3	adantr	$⊢ (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A)) \to A \in On$
232		onsseleq	$⊢ (x \cup ⋃_{y \in x} card (R_{1} (y)) \in On \land A \in On) \to (x \cup ⋃_{y \in x} card (R_{1} (y)) \subseteq A \leftrightarrow (x \cup ⋃_{y \in x} card (R_{1} (y)) \in A \lor x \cup ⋃_{y \in x} card (R_{1} (y)) = A))$
233	230 231 232	syl2an	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (x \cup ⋃_{y \in x} card (R_{1} (y)) \subseteq A \leftrightarrow (x \cup ⋃_{y \in x} card (R_{1} (y)) \in A \lor x \cup ⋃_{y \in x} card (R_{1} (y)) = A))$
234	215 233	mpbid	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (x \cup ⋃_{y \in x} card (R_{1} (y)) \in A \lor x \cup ⋃_{y \in x} card (R_{1} (y)) = A)$
235	234	orcomd	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (x \cup ⋃_{y \in x} card (R_{1} (y)) = A \lor x \cup ⋃_{y \in x} card (R_{1} (y)) \in A)$
236	235	ord	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (\neg x \cup ⋃_{y \in x} card (R_{1} (y)) = A \to x \cup ⋃_{y \in x} card (R_{1} (y)) \in A)$
237	206 236	mpd	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to x \cup ⋃_{y \in x} card (R_{1} (y)) \in A$
238	137	ad2antrl	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to card (A) = A$
239		iscard	$⊢ card (A) = A \leftrightarrow (A \in On \land \forall z \in A z ≺ A)$
240	239	simprbi	$⊢ card (A) = A \to \forall z \in A z ≺ A$
241		breq1	$⊢ z = x \cup ⋃_{y \in x} card (R_{1} (y)) \to (z ≺ A \leftrightarrow (x \cup ⋃_{y \in x} card (R_{1} (y))) ≺ A)$
242	241	rspccv	$⊢ \forall z \in A z ≺ A \to (x \cup ⋃_{y \in x} card (R_{1} (y)) \in A \to (x \cup ⋃_{y \in x} card (R_{1} (y))) ≺ A)$
243	238 240 242	3syl	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (x \cup ⋃_{y \in x} card (R_{1} (y)) \in A \to (x \cup ⋃_{y \in x} card (R_{1} (y))) ≺ A)$
244	237 243	mpd	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to (x \cup ⋃_{y \in x} card (R_{1} (y))) ≺ A$
245		domsdomtr	$⊢ (R_{1} (x) ≼ (x \cup ⋃_{y \in x} card (R_{1} (y))) \land (x \cup ⋃_{y \in x} card (R_{1} (y))) ≺ A) \to R_{1} (x) ≺ A$
246	107 244 245	syl2anc	$⊢ ((x \in A \land Lim x) \land (A \in Inacc \land \forall y \in x (y \in A \to R_{1} (y) ≺ A))) \to R_{1} (x) ≺ A$
247	246	exp43	$⊢ x \in A \to (Lim x \to (A \in Inacc \to (\forall y \in x (y \in A \to R_{1} (y) ≺ A) \to R_{1} (x) ≺ A)))$
248	247	com4l	$⊢ Lim x \to (A \in Inacc \to (\forall y \in x (y \in A \to R_{1} (y) ≺ A) \to (x \in A \to R_{1} (x) ≺ A)))$
249	13 17 21 28 61 248	tfinds2	$⊢ x \in On \to (A \in Inacc \to (x \in A \to R_{1} (x) ≺ A))$
250	249	impd	$⊢ x \in On \to ((A \in Inacc \land x \in A) \to R_{1} (x) ≺ A)$
251	9 250	mpcom	$⊢ (A \in Inacc \land x \in A) \to R_{1} (x) ≺ A$
252		sdomdom	$⊢ R_{1} (x) ≺ A \to R_{1} (x) ≼ A$
253	251 252	syl	$⊢ (A \in Inacc \land x \in A) \to R_{1} (x) ≼ A$
254	253	ralrimiva	$⊢ A \in Inacc \to \forall x \in A R_{1} (x) ≼ A$
255		iundom	$⊢ (A \in On \land \forall x \in A R_{1} (x) ≼ A) \to ⋃_{x \in A} R_{1} (x) ≼ (A \times A)$
256	3 254 255	syl2anc	$⊢ A \in Inacc \to ⋃_{x \in A} R_{1} (x) ≼ (A \times A)$
257	7 256	eqbrtrd	$⊢ A \in Inacc \to R_{1} (A) ≼ (A \times A)$
258		winainf	$⊢ A \in {Inacc}_{𝑤} \to ω \subseteq A$
259	1 258	syl	$⊢ A \in Inacc \to ω \subseteq A$
260		infxpen	$⊢ (A \in On \land ω \subseteq A) \to (A \times A) \approx A$
261	3 259 260	syl2anc	$⊢ A \in Inacc \to (A \times A) \approx A$
262		domentr	$⊢ (R_{1} (A) ≼ (A \times A) \land (A \times A) \approx A) \to R_{1} (A) ≼ A$
263	257 261 262	syl2anc	$⊢ A \in Inacc \to R_{1} (A) ≼ A$
264		fvex	$⊢ R_{1} (A) \in V$
265	122	fdmi	$⊢ dom R_{1} = On$
266	2 265	eleqtrrdi	$⊢ A \in {Inacc}_{𝑤} \to A \in dom R_{1}$
267		onssr1	$⊢ A \in dom R_{1} \to A \subseteq R_{1} (A)$
268	1 266 267	3syl	$⊢ A \in Inacc \to A \subseteq R_{1} (A)$
269		ssdomg	$⊢ R_{1} (A) \in V \to (A \subseteq R_{1} (A) \to A ≼ R_{1} (A))$
270	264 268 269	mpsyl	$⊢ A \in Inacc \to A ≼ R_{1} (A)$
271		sbth	$⊢ (R_{1} (A) ≼ A \land A ≼ R_{1} (A)) \to R_{1} (A) \approx A$
272	263 270 271	syl2anc	$⊢ A \in Inacc \to R_{1} (A) \approx A$

Metamath Proof Explorer

Theorem inar1

Proof