ttukeylem6

	Ref	Expression
Hypotheses	ttukeylem.1	$⊢ φ \to F : card (⋃ A ∖ B) \underset{1-1 onto}{⟶} ⋃ A ∖ B$
	ttukeylem.2	$⊢ φ \to B \in A$
	ttukeylem.3	$⊢ φ \to \forall x (x \in A \leftrightarrow 𝒫 x \cap Fin \subseteq A)$
	ttukeylem.4	$⊢ G = recs ((z \in V ⟼ if (dom z = ⋃ dom z, if (dom z = \emptyset, B, ⋃ ran z), z (⋃ dom z) \cup if (z (⋃ dom z) \cup \{F (⋃ dom z)\} \in A, \{F (⋃ dom z)\}, \emptyset))))$
Assertion	ttukeylem6	$⊢ (φ \land C \in suc card (⋃ A ∖ B)) \to G (C) \in A$

Proof

Step	Hyp	Ref	Expression
1		ttukeylem.1	$⊢ φ \to F : card (⋃ A ∖ B) \underset{1-1 onto}{⟶} ⋃ A ∖ B$
2		ttukeylem.2	$⊢ φ \to B \in A$
3		ttukeylem.3	$⊢ φ \to \forall x (x \in A \leftrightarrow 𝒫 x \cap Fin \subseteq A)$
4		ttukeylem.4	$⊢ G = recs ((z \in V ⟼ if (dom z = ⋃ dom z, if (dom z = \emptyset, B, ⋃ ran z), z (⋃ dom z) \cup if (z (⋃ dom z) \cup \{F (⋃ dom z)\} \in A, \{F (⋃ dom z)\}, \emptyset))))$
5		cardon	$⊢ card (⋃ A ∖ B) \in On$
6	5	onsuci	$⊢ suc card (⋃ A ∖ B) \in On$
7	6	a1i	$⊢ φ \to suc card (⋃ A ∖ B) \in On$
8		onelon	$⊢ (suc card (⋃ A ∖ B) \in On \land C \in suc card (⋃ A ∖ B)) \to C \in On$
9	7 8	sylan	$⊢ (φ \land C \in suc card (⋃ A ∖ B)) \to C \in On$
10		eleq1	$⊢ y = a \to (y \in suc card (⋃ A ∖ B) \leftrightarrow a \in suc card (⋃ A ∖ B))$
11		fveq2	$⊢ y = a \to G (y) = G (a)$
12	11	eleq1d	$⊢ y = a \to (G (y) \in A \leftrightarrow G (a) \in A)$
13	10 12	imbi12d	$⊢ y = a \to ((y \in suc card (⋃ A ∖ B) \to G (y) \in A) \leftrightarrow (a \in suc card (⋃ A ∖ B) \to G (a) \in A))$
14	13	imbi2d	$⊢ y = a \to ((φ \to (y \in suc card (⋃ A ∖ B) \to G (y) \in A)) \leftrightarrow (φ \to (a \in suc card (⋃ A ∖ B) \to G (a) \in A)))$
15		eleq1	$⊢ y = C \to (y \in suc card (⋃ A ∖ B) \leftrightarrow C \in suc card (⋃ A ∖ B))$
16		fveq2	$⊢ y = C \to G (y) = G (C)$
17	16	eleq1d	$⊢ y = C \to (G (y) \in A \leftrightarrow G (C) \in A)$
18	15 17	imbi12d	$⊢ y = C \to ((y \in suc card (⋃ A ∖ B) \to G (y) \in A) \leftrightarrow (C \in suc card (⋃ A ∖ B) \to G (C) \in A))$
19	18	imbi2d	$⊢ y = C \to ((φ \to (y \in suc card (⋃ A ∖ B) \to G (y) \in A)) \leftrightarrow (φ \to (C \in suc card (⋃ A ∖ B) \to G (C) \in A)))$
20		r19.21v	$⊢ \forall a \in y (φ \to (a \in suc card (⋃ A ∖ B) \to G (a) \in A)) \leftrightarrow (φ \to \forall a \in y (a \in suc card (⋃ A ∖ B) \to G (a) \in A))$
21	6	onordi	$⊢ Ord suc card (⋃ A ∖ B)$
22	21	a1i	$⊢ φ \to Ord suc card (⋃ A ∖ B)$
23		ordelss	$⊢ (Ord suc card (⋃ A ∖ B) \land y \in suc card (⋃ A ∖ B)) \to y \subseteq suc card (⋃ A ∖ B)$
24	22 23	sylan	$⊢ (φ \land y \in suc card (⋃ A ∖ B)) \to y \subseteq suc card (⋃ A ∖ B)$
25	24	sselda	$⊢ ((φ \land y \in suc card (⋃ A ∖ B)) \land a \in y) \to a \in suc card (⋃ A ∖ B)$
26		biimt	$⊢ a \in suc card (⋃ A ∖ B) \to (G (a) \in A \leftrightarrow (a \in suc card (⋃ A ∖ B) \to G (a) \in A))$
27	25 26	syl	$⊢ ((φ \land y \in suc card (⋃ A ∖ B)) \land a \in y) \to (G (a) \in A \leftrightarrow (a \in suc card (⋃ A ∖ B) \to G (a) \in A))$
28	27	ralbidva	$⊢ (φ \land y \in suc card (⋃ A ∖ B)) \to (\forall a \in y G (a) \in A \leftrightarrow \forall a \in y (a \in suc card (⋃ A ∖ B) \to G (a) \in A))$
29	6	onssi	$⊢ suc card (⋃ A ∖ B) \subseteq On$
30		simprl	$⊢ (φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \to y \in suc card (⋃ A ∖ B)$
31	29 30	sselid	$⊢ (φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \to y \in On$
32	1 2 3 4	ttukeylem3	$⊢ (φ \land y \in On) \to G (y) = if (y = ⋃ y, if (y = \emptyset, B, ⋃ G [y]), G (⋃ y) \cup if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset))$
33	31 32	syldan	$⊢ (φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \to G (y) = if (y = ⋃ y, if (y = \emptyset, B, ⋃ G [y]), G (⋃ y) \cup if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset))$
34	2	ad3antrrr	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land y = \emptyset) \to B \in A$
35		simpr	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to w \in (𝒫 ⋃ G [y] \cap Fin)$
36	35	elin2d	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to w \in Fin$
37	35	elin1d	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to w \in 𝒫 ⋃ G [y]$
38	37	elpwid	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to w \subseteq ⋃ G [y]$
39	4	tfr1	$⊢ G Fn On$
40		fnfun	$⊢ G Fn On \to Fun G$
41		funiunfv	$⊢ Fun G \to ⋃_{v \in y} G (v) = ⋃ G [y]$
42	39 40 41	mp2b	$⊢ ⋃_{v \in y} G (v) = ⋃ G [y]$
43	38 42	sseqtrrdi	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to w \subseteq ⋃_{v \in y} G (v)$
44		dfss3	$⊢ w \subseteq ⋃_{v \in y} G (v) \leftrightarrow \forall u \in w u \in ⋃_{v \in y} G (v)$
45		eliun	$⊢ u \in ⋃_{v \in y} G (v) \leftrightarrow \exists v \in y u \in G (v)$
46	45	ralbii	$⊢ \forall u \in w u \in ⋃_{v \in y} G (v) \leftrightarrow \forall u \in w \exists v \in y u \in G (v)$
47	44 46	bitri	$⊢ w \subseteq ⋃_{v \in y} G (v) \leftrightarrow \forall u \in w \exists v \in y u \in G (v)$
48	43 47	sylib	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to \forall u \in w \exists v \in y u \in G (v)$
49		fveq2	$⊢ v = f (u) \to G (v) = G (f (u))$
50	49	eleq2d	$⊢ v = f (u) \to (u \in G (v) \leftrightarrow u \in G (f (u)))$
51	50	ac6sfi	$⊢ (w \in Fin \land \forall u \in w \exists v \in y u \in G (v)) \to \exists f (f : w ⟶ y \land \forall u \in w u \in G (f (u)))$
52	36 48 51	syl2anc	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to \exists f (f : w ⟶ y \land \forall u \in w u \in G (f (u)))$
53		eleq1	$⊢ w = \emptyset \to (w \in A \leftrightarrow \emptyset \in A)$
54		simp-4l	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to φ$
55		fveq2	$⊢ a = ⋃ ran f \to G (a) = G (⋃ ran f)$
56	55	eleq1d	$⊢ a = ⋃ ran f \to (G (a) \in A \leftrightarrow G (⋃ ran f) \in A)$
57		simplrr	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \to \forall a \in y G (a) \in A$
58	57	ad2antrr	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to \forall a \in y G (a) \in A$
59		simprrl	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \to f : w ⟶ y$
60	59	adantr	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to f : w ⟶ y$
61		frn	$⊢ f : w ⟶ y \to ran f \subseteq y$
62	60 61	syl	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to ran f \subseteq y$
63	31	ad3antrrr	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to y \in On$
64		onss	$⊢ y \in On \to y \subseteq On$
65	63 64	syl	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to y \subseteq On$
66	62 65	sstrd	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to ran f \subseteq On$
67	36	adantrr	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \to w \in Fin$
68	67	adantr	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to w \in Fin$
69		ffn	$⊢ f : w ⟶ y \to f Fn w$
70	60 69	syl	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to f Fn w$
71		dffn4	$⊢ f Fn w \leftrightarrow f : w \underset{onto}{⟶} ran f$
72	70 71	sylib	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to f : w \underset{onto}{⟶} ran f$
73		fofi	$⊢ (w \in Fin \land f : w \underset{onto}{⟶} ran f) \to ran f \in Fin$
74	68 72 73	syl2anc	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to ran f \in Fin$
75		dm0rn0	$⊢ dom f = \emptyset \leftrightarrow ran f = \emptyset$
76	59	fdmd	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \to dom f = w$
77	76	eqeq1d	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \to (dom f = \emptyset \leftrightarrow w = \emptyset)$
78	75 77	bitr3id	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \to (ran f = \emptyset \leftrightarrow w = \emptyset)$
79	78	necon3bid	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \to (ran f \neq \emptyset \leftrightarrow w \neq \emptyset)$
80	79	biimpar	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to ran f \neq \emptyset$
81		ordunifi	$⊢ (ran f \subseteq On \land ran f \in Fin \land ran f \neq \emptyset) \to ⋃ ran f \in ran f$
82	66 74 80 81	syl3anc	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to ⋃ ran f \in ran f$
83	62 82	sseldd	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to ⋃ ran f \in y$
84	56 58 83	rspcdva	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to G (⋃ ran f) \in A$
85		simp-4l	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to φ$
86	31	ad3antrrr	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to y \in On$
87	86 64	syl	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to y \subseteq On$
88		ffvelrn	$⊢ (f : w ⟶ y \land u \in w) \to f (u) \in y$
89	88	adantl	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to f (u) \in y$
90	87 89	sseldd	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to f (u) \in On$
91	61	ad2antrl	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to ran f \subseteq y$
92	91 87	sstrd	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to ran f \subseteq On$
93		vex	$⊢ f \in V$
94	93	rnex	$⊢ ran f \in V$
95	94	ssonunii	$⊢ ran f \subseteq On \to ⋃ ran f \in On$
96	92 95	syl	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to ⋃ ran f \in On$
97	69	ad2antrl	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to f Fn w$
98		simprr	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to u \in w$
99		fnfvelrn	$⊢ (f Fn w \land u \in w) \to f (u) \in ran f$
100	97 98 99	syl2anc	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to f (u) \in ran f$
101		elssuni	$⊢ f (u) \in ran f \to f (u) \subseteq ⋃ ran f$
102	100 101	syl	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to f (u) \subseteq ⋃ ran f$
103	1 2 3 4	ttukeylem5	$⊢ (φ \land (f (u) \in On \land ⋃ ran f \in On \land f (u) \subseteq ⋃ ran f)) \to G (f (u)) \subseteq G (⋃ ran f)$
104	85 90 96 102 103	syl13anc	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to G (f (u)) \subseteq G (⋃ ran f)$
105	104	sseld	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land (f : w ⟶ y \land u \in w)) \to (u \in G (f (u)) \to u \in G (⋃ ran f))$
106	105	anassrs	$⊢ (((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land f : w ⟶ y) \land u \in w) \to (u \in G (f (u)) \to u \in G (⋃ ran f))$
107	106	ralimdva	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \land f : w ⟶ y) \to (\forall u \in w u \in G (f (u)) \to \forall u \in w u \in G (⋃ ran f))$
108	107	expimpd	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to ((f : w ⟶ y \land \forall u \in w u \in G (f (u))) \to \forall u \in w u \in G (⋃ ran f))$
109	108	impr	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \to \forall u \in w u \in G (⋃ ran f)$
110	109	adantr	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to \forall u \in w u \in G (⋃ ran f)$
111		dfss3	$⊢ w \subseteq G (⋃ ran f) \leftrightarrow \forall u \in w u \in G (⋃ ran f)$
112	110 111	sylibr	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to w \subseteq G (⋃ ran f)$
113	1 2 3	ttukeylem2	$⊢ (φ \land (G (⋃ ran f) \in A \land w \subseteq G (⋃ ran f))) \to w \in A$
114	54 84 112 113	syl12anc	$⊢ ((((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \land w \neq \emptyset) \to w \in A$
115		0ss	$⊢ \emptyset \subseteq B$
116	1 2 3	ttukeylem2	$⊢ (φ \land (B \in A \land \emptyset \subseteq B)) \to \emptyset \in A$
117	115 116	mpanr2	$⊢ (φ \land B \in A) \to \emptyset \in A$
118	2 117	mpdan	$⊢ φ \to \emptyset \in A$
119	118	ad3antrrr	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \to \emptyset \in A$
120	53 114 119	pm2.61ne	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land (w \in (𝒫 ⋃ G [y] \cap Fin) \land (f : w ⟶ y \land \forall u \in w u \in G (f (u))))) \to w \in A$
121	120	expr	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to ((f : w ⟶ y \land \forall u \in w u \in G (f (u))) \to w \in A)$
122	121	exlimdv	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to (\exists f (f : w ⟶ y \land \forall u \in w u \in G (f (u))) \to w \in A)$
123	52 122	mpd	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land w \in (𝒫 ⋃ G [y] \cap Fin)) \to w \in A$
124	123	ex	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \to (w \in (𝒫 ⋃ G [y] \cap Fin) \to w \in A)$
125	124	ssrdv	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \to 𝒫 ⋃ G [y] \cap Fin \subseteq A$
126	1 2 3	ttukeylem1	$⊢ φ \to (⋃ G [y] \in A \leftrightarrow 𝒫 ⋃ G [y] \cap Fin \subseteq A)$
127	126	ad2antrr	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \to (⋃ G [y] \in A \leftrightarrow 𝒫 ⋃ G [y] \cap Fin \subseteq A)$
128	125 127	mpbird	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \to ⋃ G [y] \in A$
129	128	adantr	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \land \neg y = \emptyset) \to ⋃ G [y] \in A$
130	34 129	ifclda	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land y = ⋃ y) \to if (y = \emptyset, B, ⋃ G [y]) \in A$
131		uneq2	$⊢ \{F (⋃ y)\} = if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset) \to G (⋃ y) \cup \{F (⋃ y)\} = G (⋃ y) \cup if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset)$
132	131	eleq1d	$⊢ \{F (⋃ y)\} = if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset) \to (G (⋃ y) \cup \{F (⋃ y)\} \in A \leftrightarrow G (⋃ y) \cup if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset) \in A)$
133		un0	$⊢ G (⋃ y) \cup \emptyset = G (⋃ y)$
134		uneq2	$⊢ \emptyset = if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset) \to G (⋃ y) \cup \emptyset = G (⋃ y) \cup if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset)$
135	133 134	eqtr3id	$⊢ \emptyset = if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset) \to G (⋃ y) = G (⋃ y) \cup if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset)$
136	135	eleq1d	$⊢ \emptyset = if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset) \to (G (⋃ y) \in A \leftrightarrow G (⋃ y) \cup if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset) \in A)$
137		simpr	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land \neg y = ⋃ y) \land G (⋃ y) \cup \{F (⋃ y)\} \in A) \to G (⋃ y) \cup \{F (⋃ y)\} \in A$
138		fveq2	$⊢ a = ⋃ y \to G (a) = G (⋃ y)$
139	138	eleq1d	$⊢ a = ⋃ y \to (G (a) \in A \leftrightarrow G (⋃ y) \in A)$
140		simplrr	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land \neg y = ⋃ y) \to \forall a \in y G (a) \in A$
141		vuniex	$⊢ ⋃ y \in V$
142	141	sucid	$⊢ ⋃ y \in suc ⋃ y$
143		eloni	$⊢ y \in On \to Ord y$
144		orduniorsuc	$⊢ Ord y \to (y = ⋃ y \lor y = suc ⋃ y)$
145	31 143 144	3syl	$⊢ (φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \to (y = ⋃ y \lor y = suc ⋃ y)$
146	145	orcanai	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land \neg y = ⋃ y) \to y = suc ⋃ y$
147	142 146	eleqtrrid	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land \neg y = ⋃ y) \to ⋃ y \in y$
148	139 140 147	rspcdva	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land \neg y = ⋃ y) \to G (⋃ y) \in A$
149	148	adantr	$⊢ (((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land \neg y = ⋃ y) \land \neg G (⋃ y) \cup \{F (⋃ y)\} \in A) \to G (⋃ y) \in A$
150	132 136 137 149	ifbothda	$⊢ ((φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \land \neg y = ⋃ y) \to G (⋃ y) \cup if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset) \in A$
151	130 150	ifclda	$⊢ (φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \to if (y = ⋃ y, if (y = \emptyset, B, ⋃ G [y]), G (⋃ y) \cup if (G (⋃ y) \cup \{F (⋃ y)\} \in A, \{F (⋃ y)\}, \emptyset)) \in A$
152	33 151	eqeltrd	$⊢ (φ \land (y \in suc card (⋃ A ∖ B) \land \forall a \in y G (a) \in A)) \to G (y) \in A$
153	152	expr	$⊢ (φ \land y \in suc card (⋃ A ∖ B)) \to (\forall a \in y G (a) \in A \to G (y) \in A)$
154	28 153	sylbird	$⊢ (φ \land y \in suc card (⋃ A ∖ B)) \to (\forall a \in y (a \in suc card (⋃ A ∖ B) \to G (a) \in A) \to G (y) \in A)$
155	154	ex	$⊢ φ \to (y \in suc card (⋃ A ∖ B) \to (\forall a \in y (a \in suc card (⋃ A ∖ B) \to G (a) \in A) \to G (y) \in A))$
156	155	com23	$⊢ φ \to (\forall a \in y (a \in suc card (⋃ A ∖ B) \to G (a) \in A) \to (y \in suc card (⋃ A ∖ B) \to G (y) \in A))$
157	156	a2i	$⊢ (φ \to \forall a \in y (a \in suc card (⋃ A ∖ B) \to G (a) \in A)) \to (φ \to (y \in suc card (⋃ A ∖ B) \to G (y) \in A))$
158	20 157	sylbi	$⊢ \forall a \in y (φ \to (a \in suc card (⋃ A ∖ B) \to G (a) \in A)) \to (φ \to (y \in suc card (⋃ A ∖ B) \to G (y) \in A))$
159	158	a1i	$⊢ y \in On \to (\forall a \in y (φ \to (a \in suc card (⋃ A ∖ B) \to G (a) \in A)) \to (φ \to (y \in suc card (⋃ A ∖ B) \to G (y) \in A)))$
160	14 19 159	tfis3	$⊢ C \in On \to (φ \to (C \in suc card (⋃ A ∖ B) \to G (C) \in A))$
161	160	impd	$⊢ C \in On \to ((φ \land C \in suc card (⋃ A ∖ B)) \to G (C) \in A)$
162	9 161	mpcom	$⊢ (φ \land C \in suc card (⋃ A ∖ B)) \to G (C) \in A$

Metamath Proof Explorer

Theorem ttukeylem6

Proof