aomclem8

Description: Lemma for dfac11 . Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Hypotheses	aomclem8.a	$⊢ φ \to A \in On$
	aomclem8.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
Assertion	aomclem8	$⊢ φ \to \exists b b We R_{1} (A)$

Proof

Step	Hyp	Ref	Expression
1		aomclem8.a	$⊢ φ \to A \in On$
2		aomclem8.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
3		elequ2	$⊢ h = b \to (i \in h \leftrightarrow i \in b)$
4		elequ2	$⊢ g = c \to (i \in g \leftrightarrow i \in c)$
5	4	notbid	$⊢ g = c \to (\neg i \in g \leftrightarrow \neg i \in c)$
6	3 5	bi2anan9r	$⊢ (g = c \land h = b) \to ((i \in h \land \neg i \in g) \leftrightarrow (i \in b \land \neg i \in c))$
7		elequ2	$⊢ g = c \to (j \in g \leftrightarrow j \in c)$
8		elequ2	$⊢ h = b \to (j \in h \leftrightarrow j \in b)$
9	7 8	bi2bian9	$⊢ (g = c \land h = b) \to ((j \in g \leftrightarrow j \in h) \leftrightarrow (j \in c \leftrightarrow j \in b))$
10	9	imbi2d	$⊢ (g = c \land h = b) \to ((j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)) \leftrightarrow (j e (⋃ dom e) i \to (j \in c \leftrightarrow j \in b)))$
11	10	ralbidv	$⊢ (g = c \land h = b) \to (\forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)) \leftrightarrow \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in c \leftrightarrow j \in b)))$
12	6 11	anbi12d	$⊢ (g = c \land h = b) \to (((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h))) \leftrightarrow ((i \in b \land \neg i \in c) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in c \leftrightarrow j \in b))))$
13	12	rexbidv	$⊢ (g = c \land h = b) \to (\exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h))) \leftrightarrow \exists i \in R_{1} (⋃ dom e) ((i \in b \land \neg i \in c) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in c \leftrightarrow j \in b))))$
14		elequ1	$⊢ i = d \to (i \in b \leftrightarrow d \in b)$
15		elequ1	$⊢ i = d \to (i \in c \leftrightarrow d \in c)$
16	15	notbid	$⊢ i = d \to (\neg i \in c \leftrightarrow \neg d \in c)$
17	14 16	anbi12d	$⊢ i = d \to ((i \in b \land \neg i \in c) \leftrightarrow (d \in b \land \neg d \in c))$
18		breq2	$⊢ i = d \to (j e (⋃ dom e) i \leftrightarrow j e (⋃ dom e) d)$
19	18	imbi1d	$⊢ i = d \to ((j e (⋃ dom e) i \to (j \in c \leftrightarrow j \in b)) \leftrightarrow (j e (⋃ dom e) d \to (j \in c \leftrightarrow j \in b)))$
20	19	ralbidv	$⊢ i = d \to (\forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in c \leftrightarrow j \in b)) \leftrightarrow \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) d \to (j \in c \leftrightarrow j \in b)))$
21		breq1	$⊢ j = f \to (j e (⋃ dom e) d \leftrightarrow f e (⋃ dom e) d)$
22		elequ1	$⊢ j = f \to (j \in c \leftrightarrow f \in c)$
23		elequ1	$⊢ j = f \to (j \in b \leftrightarrow f \in b)$
24	22 23	bibi12d	$⊢ j = f \to ((j \in c \leftrightarrow j \in b) \leftrightarrow (f \in c \leftrightarrow f \in b))$
25	21 24	imbi12d	$⊢ j = f \to ((j e (⋃ dom e) d \to (j \in c \leftrightarrow j \in b)) \leftrightarrow (f e (⋃ dom e) d \to (f \in c \leftrightarrow f \in b)))$
26	25	cbvralvw	$⊢ \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) d \to (j \in c \leftrightarrow j \in b)) \leftrightarrow \forall f \in R_{1} (⋃ dom e) (f e (⋃ dom e) d \to (f \in c \leftrightarrow f \in b))$
27	20 26	syl6bb	$⊢ i = d \to (\forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in c \leftrightarrow j \in b)) \leftrightarrow \forall f \in R_{1} (⋃ dom e) (f e (⋃ dom e) d \to (f \in c \leftrightarrow f \in b)))$
28	17 27	anbi12d	$⊢ i = d \to (((i \in b \land \neg i \in c) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in c \leftrightarrow j \in b))) \leftrightarrow ((d \in b \land \neg d \in c) \land \forall f \in R_{1} (⋃ dom e) (f e (⋃ dom e) d \to (f \in c \leftrightarrow f \in b))))$
29	28	cbvrexvw	$⊢ \exists i \in R_{1} (⋃ dom e) ((i \in b \land \neg i \in c) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in c \leftrightarrow j \in b))) \leftrightarrow \exists d \in R_{1} (⋃ dom e) ((d \in b \land \neg d \in c) \land \forall f \in R_{1} (⋃ dom e) (f e (⋃ dom e) d \to (f \in c \leftrightarrow f \in b)))$
30	13 29	syl6bb	$⊢ (g = c \land h = b) \to (\exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h))) \leftrightarrow \exists d \in R_{1} (⋃ dom e) ((d \in b \land \neg d \in c) \land \forall f \in R_{1} (⋃ dom e) (f e (⋃ dom e) d \to (f \in c \leftrightarrow f \in b))))$
31	30	cbvopabv	$⊢ \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\} = \{⟨c, b⟩ \| \exists d \in R_{1} (⋃ dom e) ((d \in b \land \neg d \in c) \land \forall f \in R_{1} (⋃ dom e) (f e (⋃ dom e) d \to (f \in c \leftrightarrow f \in b)))\}$
32		nfcv	$⊢ \underline{Ⅎ} c sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})$
33		nfcv	$⊢ \underline{Ⅎ} g y (c)$
34		nfcv	$⊢ \underline{Ⅎ} g R_{1} (dom e)$
35		nfopab1	$⊢ \underline{Ⅎ} g \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\}$
36	33 34 35	nfsup	$⊢ \underline{Ⅎ} g sup (y (c), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})$
37		fveq2	$⊢ g = c \to y (g) = y (c)$
38	37	supeq1d	$⊢ g = c \to sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\}) = sup (y (c), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})$
39	32 36 38	cbvmpt	$⊢ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) = (c \in V ⟼ sup (y (c), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\}))$
40		nfcv	$⊢ \underline{Ⅎ} c (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)$
41		nffvmpt1	$⊢ \underline{Ⅎ} g (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran c)$
42		rneq	$⊢ g = c \to ran g = ran c$
43	42	difeq2d	$⊢ g = c \to R_{1} (dom e) ∖ ran g = R_{1} (dom e) ∖ ran c$
44	43	fveq2d	$⊢ g = c \to (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g) = (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran c)$
45	40 41 44	cbvmpt	$⊢ (g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)) = (c \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran c))$
46		recseq	$⊢ (g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)) = (c \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran c)) \to recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g))) = recs ((c \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran c)))$
47	45 46	ax-mp	$⊢ recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g))) = recs ((c \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran c)))$
48		nfv	$⊢ Ⅎ c ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]$
49		nfv	$⊢ Ⅎ b ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]$
50		nfmpt1	$⊢ \underline{Ⅎ} g (g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g))$
51	50	nfrecs	$⊢ \underline{Ⅎ} g recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))$
52	51	nfcnv	$⊢ \underline{Ⅎ} g {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1}$
53		nfcv	$⊢ \underline{Ⅎ} g \{c\}$
54	52 53	nfima	$⊢ \underline{Ⅎ} g {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}]$
55	54	nfint	$⊢ \underline{Ⅎ} g ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}]$
56		nfcv	$⊢ \underline{Ⅎ} g \{b\}$
57	52 56	nfima	$⊢ \underline{Ⅎ} g {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]$
58	57	nfint	$⊢ \underline{Ⅎ} g ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]$
59	55 58	nfel	$⊢ Ⅎ g ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]$
60		nfcv	$⊢ \underline{Ⅎ} h V$
61		nfcv	$⊢ \underline{Ⅎ} h y (g)$
62		nfcv	$⊢ \underline{Ⅎ} h R_{1} (dom e)$
63		nfopab2	$⊢ \underline{Ⅎ} h \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\}$
64	61 62 63	nfsup	$⊢ \underline{Ⅎ} h sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})$
65	60 64	nfmpt	$⊢ \underline{Ⅎ} h (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\}))$
66		nfcv	$⊢ \underline{Ⅎ} h (R_{1} (dom e) ∖ ran g)$
67	65 66	nffv	$⊢ \underline{Ⅎ} h (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)$
68	60 67	nfmpt	$⊢ \underline{Ⅎ} h (g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g))$
69	68	nfrecs	$⊢ \underline{Ⅎ} h recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))$
70	69	nfcnv	$⊢ \underline{Ⅎ} h {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1}$
71		nfcv	$⊢ \underline{Ⅎ} h \{c\}$
72	70 71	nfima	$⊢ \underline{Ⅎ} h {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}]$
73	72	nfint	$⊢ \underline{Ⅎ} h ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}]$
74		nfcv	$⊢ \underline{Ⅎ} h \{b\}$
75	70 74	nfima	$⊢ \underline{Ⅎ} h {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]$
76	75	nfint	$⊢ \underline{Ⅎ} h ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]$
77	73 76	nfel	$⊢ Ⅎ h ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]$
78		sneq	$⊢ g = c \to \{g\} = \{c\}$
79	78	imaeq2d	$⊢ g = c \to {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] = {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}]$
80	79	inteqd	$⊢ g = c \to ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] = ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}]$
81		sneq	$⊢ h = b \to \{h\} = \{b\}$
82	81	imaeq2d	$⊢ h = b \to {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}] = {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]$
83	82	inteqd	$⊢ h = b \to ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}] = ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]$
84		eleq12	$⊢ (⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] = ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}] \land ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}] = ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]) \to (⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}] \leftrightarrow ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}])$
85	80 83 84	syl2an	$⊢ (g = c \land h = b) \to (⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}] \leftrightarrow ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}])$
86	48 49 59 77 85	cbvopab	$⊢ \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\} = \{⟨c, b⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{c\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{b\}]\}$
87		fveq2	$⊢ g = c \to rank (g) = rank (c)$
88		fveq2	$⊢ h = b \to rank (h) = rank (b)$
89	87 88	breqan12d	$⊢ (g = c \land h = b) \to (rank (g) E rank (h) \leftrightarrow rank (c) E rank (b))$
90	87 88	eqeqan12d	$⊢ (g = c \land h = b) \to (rank (g) = rank (h) \leftrightarrow rank (c) = rank (b))$
91		simpl	$⊢ (g = c \land h = b) \to g = c$
92		suceq	$⊢ rank (g) = rank (c) \to suc rank (g) = suc rank (c)$
93	87 92	syl	$⊢ g = c \to suc rank (g) = suc rank (c)$
94	93	adantr	$⊢ (g = c \land h = b) \to suc rank (g) = suc rank (c)$
95	94	fveq2d	$⊢ (g = c \land h = b) \to e (suc rank (g)) = e (suc rank (c))$
96		simpr	$⊢ (g = c \land h = b) \to h = b$
97	91 95 96	breq123d	$⊢ (g = c \land h = b) \to (g e (suc rank (g)) h \leftrightarrow c e (suc rank (c)) b)$
98	90 97	anbi12d	$⊢ (g = c \land h = b) \to ((rank (g) = rank (h) \land g e (suc rank (g)) h) \leftrightarrow (rank (c) = rank (b) \land c e (suc rank (c)) b))$
99	89 98	orbi12d	$⊢ (g = c \land h = b) \to ((rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h)) \leftrightarrow (rank (c) E rank (b) \lor (rank (c) = rank (b) \land c e (suc rank (c)) b)))$
100	99	cbvopabv	$⊢ \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\} = \{⟨c, b⟩ \| (rank (c) E rank (b) \lor (rank (c) = rank (b) \land c e (suc rank (c)) b))\}$
101		eqid	$⊢ if (dom e = ⋃ dom e, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom e) \times R_{1} (dom e)) = if (dom e = ⋃ dom e, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom e) \times R_{1} (dom e))$
102		dmeq	$⊢ l = e \to dom l = dom e$
103	102	unieqd	$⊢ l = e \to ⋃ dom l = ⋃ dom e$
104	102 103	eqeq12d	$⊢ l = e \to (dom l = ⋃ dom l \leftrightarrow dom e = ⋃ dom e)$
105		fveq1	$⊢ l = e \to l (suc rank (g)) = e (suc rank (g))$
106	105	breqd	$⊢ l = e \to (g l (suc rank (g)) h \leftrightarrow g e (suc rank (g)) h)$
107	106	anbi2d	$⊢ l = e \to ((rank (g) = rank (h) \land g l (suc rank (g)) h) \leftrightarrow (rank (g) = rank (h) \land g e (suc rank (g)) h))$
108	107	orbi2d	$⊢ l = e \to ((rank (g) E rank (h) \lor (rank (g) = rank (h) \land g l (suc rank (g)) h)) \leftrightarrow (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h)))$
109	108	opabbidv	$⊢ l = e \to \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g l (suc rank (g)) h))\} = \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\}$
110		eqidd	$⊢ l = e \to y (g) = y (g)$
111	102	fveq2d	$⊢ l = e \to R_{1} (dom l) = R_{1} (dom e)$
112	103	fveq2d	$⊢ l = e \to R_{1} (⋃ dom l) = R_{1} (⋃ dom e)$
113		id	$⊢ l = e \to l = e$
114	113 103	fveq12d	$⊢ l = e \to l (⋃ dom l) = e (⋃ dom e)$
115	114	breqd	$⊢ l = e \to (j l (⋃ dom l) i \leftrightarrow j e (⋃ dom e) i)$
116	115	imbi1d	$⊢ l = e \to ((j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)) \leftrightarrow (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))$
117	112 116	raleqbidv	$⊢ l = e \to (\forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)) \leftrightarrow \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))$
118	117	anbi2d	$⊢ l = e \to (((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h))) \leftrightarrow ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h))))$
119	112 118	rexeqbidv	$⊢ l = e \to (\exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h))) \leftrightarrow \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h))))$
120	119	opabbidv	$⊢ l = e \to \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\} = \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\}$
121	110 111 120	supeq123d	$⊢ l = e \to sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\}) = sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})$
122	121	mpteq2dv	$⊢ l = e \to (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) = (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\}))$
123	111	difeq1d	$⊢ l = e \to R_{1} (dom l) ∖ ran g = R_{1} (dom e) ∖ ran g$
124	122 123	fveq12d	$⊢ l = e \to (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g) = (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)$
125	124	mpteq2dv	$⊢ l = e \to (g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)) = (g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g))$
126		recseq	$⊢ (g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)) = (g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)) \to recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g))) = recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))$
127	125 126	syl	$⊢ l = e \to recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g))) = recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))$
128	127	cnveqd	$⊢ l = e \to {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} = {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1}$
129	128	imaeq1d	$⊢ l = e \to {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] = {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}]$
130	129	inteqd	$⊢ l = e \to ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] = ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}]$
131	128	imaeq1d	$⊢ l = e \to {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}] = {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]$
132	131	inteqd	$⊢ l = e \to ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}] = ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]$
133	130 132	eleq12d	$⊢ l = e \to (⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}] \leftrightarrow ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}])$
134	133	opabbidv	$⊢ l = e \to \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}]\} = \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\}$
135	104 109 134	ifbieq12d	$⊢ l = e \to if (dom l = ⋃ dom l, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g l (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}]\}) = if (dom e = ⋃ dom e, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\})$
136	111	sqxpeqd	$⊢ l = e \to R_{1} (dom l) \times R_{1} (dom l) = R_{1} (dom e) \times R_{1} (dom e)$
137	135 136	ineq12d	$⊢ l = e \to if (dom l = ⋃ dom l, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g l (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom l) \times R_{1} (dom l)) = if (dom e = ⋃ dom e, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom e) \times R_{1} (dom e))$
138	137	cbvmptv	$⊢ (l \in V ⟼ if (dom l = ⋃ dom l, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g l (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom l) \times R_{1} (dom l))) = (e \in V ⟼ if (dom e = ⋃ dom e, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom e) \times R_{1} (dom e)))$
139		recseq	$⊢ (l \in V ⟼ if (dom l = ⋃ dom l, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g l (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom l) \times R_{1} (dom l))) = (e \in V ⟼ if (dom e = ⋃ dom e, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom e) \times R_{1} (dom e))) \to recs ((l \in V ⟼ if (dom l = ⋃ dom l, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g l (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom l) \times R_{1} (dom l)))) = recs ((e \in V ⟼ if (dom e = ⋃ dom e, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom e) \times R_{1} (dom e))))$
140	138 139	ax-mp	$⊢ recs ((l \in V ⟼ if (dom l = ⋃ dom l, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g l (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom l), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom l) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom l) (j l (⋃ dom l) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom l) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom l) \times R_{1} (dom l)))) = recs ((e \in V ⟼ if (dom e = ⋃ dom e, \{⟨g, h⟩ \| (rank (g) E rank (h) \lor (rank (g) = rank (h) \land g e (suc rank (g)) h))\}, \{⟨g, h⟩ \| ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{g\}] \in ⋂ {recs ((g \in V ⟼ (g \in V ⟼ sup (y (g), R_{1} (dom e), \{⟨g, h⟩ \| \exists i \in R_{1} (⋃ dom e) ((i \in h \land \neg i \in g) \land \forall j \in R_{1} (⋃ dom e) (j e (⋃ dom e) i \to (j \in g \leftrightarrow j \in h)))\})) (R_{1} (dom e) ∖ ran g)))}^{-1} [\{h\}]\}) \cap (R_{1} (dom e) \times R_{1} (dom e))))$
141		neeq1	$⊢ a = c \to (a \neq \emptyset \leftrightarrow c \neq \emptyset)$
142		fveq2	$⊢ a = c \to y (a) = y (c)$
143		pweq	$⊢ a = c \to 𝒫 a = 𝒫 c$
144	143	ineq1d	$⊢ a = c \to 𝒫 a \cap Fin = 𝒫 c \cap Fin$
145	144	difeq1d	$⊢ a = c \to (𝒫 a \cap Fin) ∖ \{\emptyset\} = (𝒫 c \cap Fin) ∖ \{\emptyset\}$
146	142 145	eleq12d	$⊢ a = c \to (y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}) \leftrightarrow y (c) \in ((𝒫 c \cap Fin) ∖ \{\emptyset\}))$
147	141 146	imbi12d	$⊢ a = c \to ((a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\})) \leftrightarrow (c \neq \emptyset \to y (c) \in ((𝒫 c \cap Fin) ∖ \{\emptyset\})))$
148	147	cbvralvw	$⊢ \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\})) \leftrightarrow \forall c \in 𝒫 R_{1} (A) (c \neq \emptyset \to y (c) \in ((𝒫 c \cap Fin) ∖ \{\emptyset\}))$
149	2 148	sylib	$⊢ φ \to \forall c \in 𝒫 R_{1} (A) (c \neq \emptyset \to y (c) \in ((𝒫 c \cap Fin) ∖ \{\emptyset\}))$
150	31 39 47 86 100 101 140 1 149	aomclem7	$⊢ φ \to \exists b b We R_{1} (A)$

Metamath Proof Explorer

Theorem aomclem8

Proof