axdclem

		Ref	Expression
	Hypothesis	axdclem.1	$⊢ F = {rec ((y \in V ⟼ g (\{z \| y x z\})), s) ↾}_{ω}$
	Assertion	axdclem	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x \land \exists z F (K) x z) \to (K \in ω \to F (K) x F (suc K))$

Proof

Step	Hyp	Ref	Expression
1		axdclem.1	$⊢ F = {rec ((y \in V ⟼ g (\{z \| y x z\})), s) ↾}_{ω}$
2		neeq1	$⊢ y = \{z \| F (K) x z\} \to (y \neq \emptyset \leftrightarrow \{z \| F (K) x z\} \neq \emptyset)$
3		abn0	$⊢ \{z \| F (K) x z\} \neq \emptyset \leftrightarrow \exists z F (K) x z$
4	2 3	bitrdi	$⊢ y = \{z \| F (K) x z\} \to (y \neq \emptyset \leftrightarrow \exists z F (K) x z)$
5		eleq2	$⊢ y = \{z \| F (K) x z\} \to (g (y) \in y \leftrightarrow g (y) \in \{z \| F (K) x z\})$
6		breq2	$⊢ w = z \to (F (K) x w \leftrightarrow F (K) x z)$
7	6	cbvabv	$⊢ \{w \| F (K) x w\} = \{z \| F (K) x z\}$
8	7	eleq2i	$⊢ g (y) \in \{w \| F (K) x w\} \leftrightarrow g (y) \in \{z \| F (K) x z\}$
9	5 8	bitr4di	$⊢ y = \{z \| F (K) x z\} \to (g (y) \in y \leftrightarrow g (y) \in \{w \| F (K) x w\})$
10		fvex	$⊢ g (y) \in V$
11		breq2	$⊢ w = g (y) \to (F (K) x w \leftrightarrow F (K) x g (y))$
12	10 11	elab	$⊢ g (y) \in \{w \| F (K) x w\} \leftrightarrow F (K) x g (y)$
13	9 12	bitrdi	$⊢ y = \{z \| F (K) x z\} \to (g (y) \in y \leftrightarrow F (K) x g (y))$
14		fveq2	$⊢ y = \{z \| F (K) x z\} \to g (y) = g (\{z \| F (K) x z\})$
15	14	breq2d	$⊢ y = \{z \| F (K) x z\} \to (F (K) x g (y) \leftrightarrow F (K) x g (\{z \| F (K) x z\}))$
16	13 15	bitrd	$⊢ y = \{z \| F (K) x z\} \to (g (y) \in y \leftrightarrow F (K) x g (\{z \| F (K) x z\}))$
17	4 16	imbi12d	$⊢ y = \{z \| F (K) x z\} \to ((y \neq \emptyset \to g (y) \in y) \leftrightarrow (\exists z F (K) x z \to F (K) x g (\{z \| F (K) x z\})))$
18	17	rspcv	$⊢ \{z \| F (K) x z\} \in 𝒫 dom x \to (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \to (\exists z F (K) x z \to F (K) x g (\{z \| F (K) x z\})))$
19		fvex	$⊢ F (K) \in V$
20		vex	$⊢ z \in V$
21	19 20	brelrn	$⊢ F (K) x z \to z \in ran x$
22	21	abssi	$⊢ \{z \| F (K) x z\} \subseteq ran x$
23		sstr	$⊢ (\{z \| F (K) x z\} \subseteq ran x \land ran x \subseteq dom x) \to \{z \| F (K) x z\} \subseteq dom x$
24	22 23	mpan	$⊢ ran x \subseteq dom x \to \{z \| F (K) x z\} \subseteq dom x$
25		vex	$⊢ x \in V$
26	25	dmex	$⊢ dom x \in V$
27	26	elpw2	$⊢ \{z \| F (K) x z\} \in 𝒫 dom x \leftrightarrow \{z \| F (K) x z\} \subseteq dom x$
28	24 27	sylibr	$⊢ ran x \subseteq dom x \to \{z \| F (K) x z\} \in 𝒫 dom x$
29	18 28	syl11	$⊢ \forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \to (ran x \subseteq dom x \to (\exists z F (K) x z \to F (K) x g (\{z \| F (K) x z\})))$
30	29	3imp	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x \land \exists z F (K) x z) \to F (K) x g (\{z \| F (K) x z\})$
31		fvex	$⊢ g (\{z \| F (K) x z\}) \in V$
32		nfcv	$⊢ \underline{Ⅎ} y s$
33		nfcv	$⊢ \underline{Ⅎ} y K$
34		nfcv	$⊢ \underline{Ⅎ} y g (\{z \| F (K) x z\})$
35		breq1	$⊢ y = F (K) \to (y x z \leftrightarrow F (K) x z)$
36	35	abbidv	$⊢ y = F (K) \to \{z \| y x z\} = \{z \| F (K) x z\}$
37	36	fveq2d	$⊢ y = F (K) \to g (\{z \| y x z\}) = g (\{z \| F (K) x z\})$
38	32 33 34 1 37	frsucmpt	$⊢ (K \in ω \land g (\{z \| F (K) x z\}) \in V) \to F (suc K) = g (\{z \| F (K) x z\})$
39	31 38	mpan2	$⊢ K \in ω \to F (suc K) = g (\{z \| F (K) x z\})$
40	39	breq2d	$⊢ K \in ω \to (F (K) x F (suc K) \leftrightarrow F (K) x g (\{z \| F (K) x z\}))$
41	30 40	syl5ibrcom	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x \land \exists z F (K) x z) \to (K \in ω \to F (K) x F (suc K))$

Metamath Proof Explorer

Theorem axdclem

Proof