dffi3

Description: The set of finite intersections can be "constructed" inductively by iterating binary intersection _om -many times. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Hypothesis	dffi3.1	$⊢ R = (u \in V ⟼ ran (y \in u, z \in u ⟼ y \cap z))$
	Assertion	dffi3	$⊢ A \in V \to fi (A) = ⋃ rec (R, A) [ω]$

Proof

Step	Hyp	Ref	Expression
1		dffi3.1	$⊢ R = (u \in V ⟼ ran (y \in u, z \in u ⟼ y \cap z))$
2		dffi2	$⊢ A \in V \to fi (A) = ⋂ \{x \| (A \subseteq x \land \forall c \in x \forall d \in x c \cap d \in x)\}$
3		fr0g	$⊢ A \in V \to ({rec (R, A) ↾}_{ω}) (\emptyset) = A$
4		frfnom	$⊢ ({rec (R, A) ↾}_{ω}) Fn ω$
5		peano1	$⊢ \emptyset \in ω$
6		fnfvelrn	$⊢ (({rec (R, A) ↾}_{ω}) Fn ω \land \emptyset \in ω) \to ({rec (R, A) ↾}_{ω}) (\emptyset) \in ran ({rec (R, A) ↾}_{ω})$
7	4 5 6	mp2an	$⊢ ({rec (R, A) ↾}_{ω}) (\emptyset) \in ran ({rec (R, A) ↾}_{ω})$
8	3 7	eqeltrrdi	$⊢ A \in V \to A \in ran ({rec (R, A) ↾}_{ω})$
9		elssuni	$⊢ A \in ran ({rec (R, A) ↾}_{ω}) \to A \subseteq ⋃ ran ({rec (R, A) ↾}_{ω})$
10	8 9	syl	$⊢ A \in V \to A \subseteq ⋃ ran ({rec (R, A) ↾}_{ω})$
11		reeanv	$⊢ \exists m \in ω \exists n \in ω (c \in ({rec (R, A) ↾}_{ω}) (m) \land d \in ({rec (R, A) ↾}_{ω}) (n)) \leftrightarrow (\exists m \in ω c \in ({rec (R, A) ↾}_{ω}) (m) \land \exists n \in ω d \in ({rec (R, A) ↾}_{ω}) (n))$
12		eliun	$⊢ c \in ⋃_{m \in ω} ({rec (R, A) ↾}_{ω}) (m) \leftrightarrow \exists m \in ω c \in ({rec (R, A) ↾}_{ω}) (m)$
13		eliun	$⊢ d \in ⋃_{n \in ω} ({rec (R, A) ↾}_{ω}) (n) \leftrightarrow \exists n \in ω d \in ({rec (R, A) ↾}_{ω}) (n)$
14	12 13	anbi12i	$⊢ (c \in ⋃_{m \in ω} ({rec (R, A) ↾}_{ω}) (m) \land d \in ⋃_{n \in ω} ({rec (R, A) ↾}_{ω}) (n)) \leftrightarrow (\exists m \in ω c \in ({rec (R, A) ↾}_{ω}) (m) \land \exists n \in ω d \in ({rec (R, A) ↾}_{ω}) (n))$
15		fniunfv	$⊢ ({rec (R, A) ↾}_{ω}) Fn ω \to ⋃_{m \in ω} ({rec (R, A) ↾}_{ω}) (m) = ⋃ ran ({rec (R, A) ↾}_{ω})$
16	15	eleq2d	$⊢ ({rec (R, A) ↾}_{ω}) Fn ω \to (c \in ⋃_{m \in ω} ({rec (R, A) ↾}_{ω}) (m) \leftrightarrow c \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
17		fniunfv	$⊢ ({rec (R, A) ↾}_{ω}) Fn ω \to ⋃_{n \in ω} ({rec (R, A) ↾}_{ω}) (n) = ⋃ ran ({rec (R, A) ↾}_{ω})$
18	17	eleq2d	$⊢ ({rec (R, A) ↾}_{ω}) Fn ω \to (d \in ⋃_{n \in ω} ({rec (R, A) ↾}_{ω}) (n) \leftrightarrow d \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
19	16 18	anbi12d	$⊢ ({rec (R, A) ↾}_{ω}) Fn ω \to ((c \in ⋃_{m \in ω} ({rec (R, A) ↾}_{ω}) (m) \land d \in ⋃_{n \in ω} ({rec (R, A) ↾}_{ω}) (n)) \leftrightarrow (c \in ⋃ ran ({rec (R, A) ↾}_{ω}) \land d \in ⋃ ran ({rec (R, A) ↾}_{ω})))$
20	4 19	ax-mp	$⊢ (c \in ⋃_{m \in ω} ({rec (R, A) ↾}_{ω}) (m) \land d \in ⋃_{n \in ω} ({rec (R, A) ↾}_{ω}) (n)) \leftrightarrow (c \in ⋃ ran ({rec (R, A) ↾}_{ω}) \land d \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
21	11 14 20	3bitr2i	$⊢ \exists m \in ω \exists n \in ω (c \in ({rec (R, A) ↾}_{ω}) (m) \land d \in ({rec (R, A) ↾}_{ω}) (n)) \leftrightarrow (c \in ⋃ ran ({rec (R, A) ↾}_{ω}) \land d \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
22		ordom	$⊢ Ord ω$
23		ordunel	$⊢ (Ord ω \land m \in ω \land n \in ω) \to m \cup n \in ω$
24	22 23	mp3an1	$⊢ (m \in ω \land n \in ω) \to m \cup n \in ω$
25	24	adantl	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to m \cup n \in ω$
26		simprl	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to m \in ω$
27	25 26	jca	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to (m \cup n \in ω \land m \in ω)$
28		nnon	$⊢ y \in ω \to y \in On$
29		nnon	$⊢ x \in ω \to x \in On$
30	29	ad2antlr	$⊢ ((A \in V \land x \in ω) \land y \in ω) \to x \in On$
31		onsseleq	$⊢ (y \in On \land x \in On) \to (y \subseteq x \leftrightarrow (y \in x \lor y = x))$
32	28 30 31	syl2an2	$⊢ ((A \in V \land x \in ω) \land y \in ω) \to (y \subseteq x \leftrightarrow (y \in x \lor y = x))$
33		rzal	$⊢ x = \emptyset \to \forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)$
34	33	biantrud	$⊢ x = \emptyset \to (({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \leftrightarrow (({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \land \forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)))$
35		fveq2	$⊢ x = \emptyset \to ({rec (R, A) ↾}_{ω}) (x) = ({rec (R, A) ↾}_{ω}) (\emptyset)$
36	35	sseq1d	$⊢ x = \emptyset \to (({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \leftrightarrow ({rec (R, A) ↾}_{ω}) (\emptyset) \subseteq fi (A))$
37	34 36	bitr3d	$⊢ x = \emptyset \to ((({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \land \forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)) \leftrightarrow ({rec (R, A) ↾}_{ω}) (\emptyset) \subseteq fi (A))$
38		fveq2	$⊢ x = n \to ({rec (R, A) ↾}_{ω}) (x) = ({rec (R, A) ↾}_{ω}) (n)$
39	38	sseq1d	$⊢ x = n \to (({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \leftrightarrow ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A))$
40	38	sseq2d	$⊢ x = n \to (({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x) \leftrightarrow ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n))$
41	40	raleqbi1dv	$⊢ x = n \to (\forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x) \leftrightarrow \forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n))$
42	39 41	anbi12d	$⊢ x = n \to ((({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \land \forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)) \leftrightarrow (({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A) \land \forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n)))$
43		fveq2	$⊢ x = suc n \to ({rec (R, A) ↾}_{ω}) (x) = ({rec (R, A) ↾}_{ω}) (suc n)$
44	43	sseq1d	$⊢ x = suc n \to (({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \leftrightarrow ({rec (R, A) ↾}_{ω}) (suc n) \subseteq fi (A))$
45	43	sseq2d	$⊢ x = suc n \to (({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x) \leftrightarrow ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))$
46	45	raleqbi1dv	$⊢ x = suc n \to (\forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x) \leftrightarrow \forall y \in suc n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))$
47	44 46	anbi12d	$⊢ x = suc n \to ((({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \land \forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)) \leftrightarrow (({rec (R, A) ↾}_{ω}) (suc n) \subseteq fi (A) \land \forall y \in suc n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n)))$
48		ssfii	$⊢ A \in V \to A \subseteq fi (A)$
49	3 48	eqsstrd	$⊢ A \in V \to ({rec (R, A) ↾}_{ω}) (\emptyset) \subseteq fi (A)$
50		id	$⊢ x \in ({rec (R, A) ↾}_{ω}) (n) \to x \in ({rec (R, A) ↾}_{ω}) (n)$
51		eqidd	$⊢ x \in ({rec (R, A) ↾}_{ω}) (n) \to x = x$
52		ineq1	$⊢ a = x \to a \cap b = x \cap b$
53	52	eqeq2d	$⊢ a = x \to (x = a \cap b \leftrightarrow x = x \cap b)$
54		ineq2	$⊢ b = x \to x \cap b = x \cap x$
55		inidm	$⊢ x \cap x = x$
56	54 55	eqtrdi	$⊢ b = x \to x \cap b = x$
57	56	eqeq2d	$⊢ b = x \to (x = x \cap b \leftrightarrow x = x)$
58	53 57	rspc2ev	$⊢ (x \in ({rec (R, A) ↾}_{ω}) (n) \land x \in ({rec (R, A) ↾}_{ω}) (n) \land x = x) \to \exists a \in ({rec (R, A) ↾}_{ω}) (n) \exists b \in ({rec (R, A) ↾}_{ω}) (n) x = a \cap b$
59	50 50 51 58	syl3anc	$⊢ x \in ({rec (R, A) ↾}_{ω}) (n) \to \exists a \in ({rec (R, A) ↾}_{ω}) (n) \exists b \in ({rec (R, A) ↾}_{ω}) (n) x = a \cap b$
60		eqid	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) = (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b)$
61	60	rnmpo	$⊢ ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) = \{x \| \exists a \in ({rec (R, A) ↾}_{ω}) (n) \exists b \in ({rec (R, A) ↾}_{ω}) (n) x = a \cap b\}$
62	61	abeq2i	$⊢ x \in ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) \leftrightarrow \exists a \in ({rec (R, A) ↾}_{ω}) (n) \exists b \in ({rec (R, A) ↾}_{ω}) (n) x = a \cap b$
63	59 62	sylibr	$⊢ x \in ({rec (R, A) ↾}_{ω}) (n) \to x \in ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b)$
64	63	ssriv	$⊢ ({rec (R, A) ↾}_{ω}) (n) \subseteq ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b)$
65		simpl	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to n \in ω$
66		fvex	$⊢ ({rec (R, A) ↾}_{ω}) (n) \in V$
67	66	uniex	$⊢ ⋃ ({rec (R, A) ↾}_{ω}) (n) \in V$
68	67	pwex	$⊢ 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n) \in V$
69		inss1	$⊢ a \cap b \subseteq a$
70		elssuni	$⊢ a \in ({rec (R, A) ↾}_{ω}) (n) \to a \subseteq ⋃ ({rec (R, A) ↾}_{ω}) (n)$
71	70	adantr	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (n) \land b \in ({rec (R, A) ↾}_{ω}) (n)) \to a \subseteq ⋃ ({rec (R, A) ↾}_{ω}) (n)$
72	69 71	sstrid	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (n) \land b \in ({rec (R, A) ↾}_{ω}) (n)) \to a \cap b \subseteq ⋃ ({rec (R, A) ↾}_{ω}) (n)$
73		vex	$⊢ a \in V$
74	73	inex1	$⊢ a \cap b \in V$
75	74	elpw	$⊢ a \cap b \in 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n) \leftrightarrow a \cap b \subseteq ⋃ ({rec (R, A) ↾}_{ω}) (n)$
76	72 75	sylibr	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (n) \land b \in ({rec (R, A) ↾}_{ω}) (n)) \to a \cap b \in 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n)$
77	76	rgen2	$⊢ \forall a \in ({rec (R, A) ↾}_{ω}) (n) \forall b \in ({rec (R, A) ↾}_{ω}) (n) a \cap b \in 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n)$
78	60	fmpo	$⊢ \forall a \in ({rec (R, A) ↾}_{ω}) (n) \forall b \in ({rec (R, A) ↾}_{ω}) (n) a \cap b \in 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n) \leftrightarrow (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) : ({rec (R, A) ↾}_{ω}) (n) \times ({rec (R, A) ↾}_{ω}) (n) ⟶ 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n)$
79	77 78	mpbi	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) : ({rec (R, A) ↾}_{ω}) (n) \times ({rec (R, A) ↾}_{ω}) (n) ⟶ 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n)$
80		frn	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) : ({rec (R, A) ↾}_{ω}) (n) \times ({rec (R, A) ↾}_{ω}) (n) ⟶ 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n) \to ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) \subseteq 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n)$
81	79 80	ax-mp	$⊢ ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) \subseteq 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (n)$
82	68 81	ssexi	$⊢ ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) \in V$
83		nfcv	$⊢ \underline{Ⅎ} v A$
84		nfcv	$⊢ \underline{Ⅎ} v n$
85		nfcv	$⊢ \underline{Ⅎ} v ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b)$
86		mpoeq12	$⊢ (u = v \land u = v) \to (y \in u, z \in u ⟼ y \cap z) = (y \in v, z \in v ⟼ y \cap z)$
87	86	anidms	$⊢ u = v \to (y \in u, z \in u ⟼ y \cap z) = (y \in v, z \in v ⟼ y \cap z)$
88		ineq1	$⊢ y = a \to y \cap z = a \cap z$
89		ineq2	$⊢ z = b \to a \cap z = a \cap b$
90	88 89	cbvmpov	$⊢ (y \in v, z \in v ⟼ y \cap z) = (a \in v, b \in v ⟼ a \cap b)$
91	87 90	eqtrdi	$⊢ u = v \to (y \in u, z \in u ⟼ y \cap z) = (a \in v, b \in v ⟼ a \cap b)$
92	91	rneqd	$⊢ u = v \to ran (y \in u, z \in u ⟼ y \cap z) = ran (a \in v, b \in v ⟼ a \cap b)$
93	92	cbvmptv	$⊢ (u \in V ⟼ ran (y \in u, z \in u ⟼ y \cap z)) = (v \in V ⟼ ran (a \in v, b \in v ⟼ a \cap b))$
94	1 93	eqtri	$⊢ R = (v \in V ⟼ ran (a \in v, b \in v ⟼ a \cap b))$
95		rdgeq1	$⊢ R = (v \in V ⟼ ran (a \in v, b \in v ⟼ a \cap b)) \to rec (R, A) = rec ((v \in V ⟼ ran (a \in v, b \in v ⟼ a \cap b)), A)$
96	94 95	ax-mp	$⊢ rec (R, A) = rec ((v \in V ⟼ ran (a \in v, b \in v ⟼ a \cap b)), A)$
97	96	reseq1i	$⊢ {rec (R, A) ↾}_{ω} = {rec ((v \in V ⟼ ran (a \in v, b \in v ⟼ a \cap b)), A) ↾}_{ω}$
98		mpoeq12	$⊢ (v = ({rec (R, A) ↾}_{ω}) (n) \land v = ({rec (R, A) ↾}_{ω}) (n)) \to (a \in v, b \in v ⟼ a \cap b) = (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b)$
99	98	anidms	$⊢ v = ({rec (R, A) ↾}_{ω}) (n) \to (a \in v, b \in v ⟼ a \cap b) = (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b)$
100	99	rneqd	$⊢ v = ({rec (R, A) ↾}_{ω}) (n) \to ran (a \in v, b \in v ⟼ a \cap b) = ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b)$
101	83 84 85 97 100	frsucmpt	$⊢ (n \in ω \land ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) \in V) \to ({rec (R, A) ↾}_{ω}) (suc n) = ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b)$
102	65 82 101	sylancl	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to ({rec (R, A) ↾}_{ω}) (suc n) = ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b)$
103	64 102	sseqtrrid	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to ({rec (R, A) ↾}_{ω}) (n) \subseteq ({rec (R, A) ↾}_{ω}) (suc n)$
104		sstr2	$⊢ ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n) \to (({rec (R, A) ↾}_{ω}) (n) \subseteq ({rec (R, A) ↾}_{ω}) (suc n) \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))$
105	103 104	syl5com	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to (({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n) \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))$
106	105	ralimdv	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to (\forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n) \to \forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))$
107		vex	$⊢ n \in V$
108		fveq2	$⊢ y = n \to ({rec (R, A) ↾}_{ω}) (y) = ({rec (R, A) ↾}_{ω}) (n)$
109	108	sseq1d	$⊢ y = n \to (({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n) \leftrightarrow ({rec (R, A) ↾}_{ω}) (n) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))$
110	107 109	ralsn	$⊢ \forall y \in \{n\} ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n) \leftrightarrow ({rec (R, A) ↾}_{ω}) (n) \subseteq ({rec (R, A) ↾}_{ω}) (suc n)$
111	103 110	sylibr	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to \forall y \in \{n\} ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n)$
112	106 111	jctird	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to (\forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n) \to (\forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n) \land \forall y \in \{n\} ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n)))$
113		df-suc	$⊢ suc n = n \cup \{n\}$
114	113	raleqi	$⊢ \forall y \in suc n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n) \leftrightarrow \forall y \in (n \cup \{n\}) ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n)$
115		ralunb	$⊢ \forall y \in (n \cup \{n\}) ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n) \leftrightarrow (\forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n) \land \forall y \in \{n\} ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))$
116	114 115	bitri	$⊢ \forall y \in suc n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n) \leftrightarrow (\forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n) \land \forall y \in \{n\} ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))$
117	112 116	syl6ibr	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to (\forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n) \to \forall y \in suc n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))$
118		fiin	$⊢ (a \in fi (A) \land b \in fi (A)) \to a \cap b \in fi (A)$
119	118	rgen2	$⊢ \forall a \in fi (A) \forall b \in fi (A) a \cap b \in fi (A)$
120		ss2ralv	$⊢ ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A) \to (\forall a \in fi (A) \forall b \in fi (A) a \cap b \in fi (A) \to \forall a \in ({rec (R, A) ↾}_{ω}) (n) \forall b \in ({rec (R, A) ↾}_{ω}) (n) a \cap b \in fi (A))$
121	119 120	mpi	$⊢ ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A) \to \forall a \in ({rec (R, A) ↾}_{ω}) (n) \forall b \in ({rec (R, A) ↾}_{ω}) (n) a \cap b \in fi (A)$
122	60	fmpo	$⊢ \forall a \in ({rec (R, A) ↾}_{ω}) (n) \forall b \in ({rec (R, A) ↾}_{ω}) (n) a \cap b \in fi (A) \leftrightarrow (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) : ({rec (R, A) ↾}_{ω}) (n) \times ({rec (R, A) ↾}_{ω}) (n) ⟶ fi (A)$
123	121 122	sylib	$⊢ ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A) \to (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) : ({rec (R, A) ↾}_{ω}) (n) \times ({rec (R, A) ↾}_{ω}) (n) ⟶ fi (A)$
124	123	frnd	$⊢ ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A) \to ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) \subseteq fi (A)$
125	124	adantl	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to ran (a \in ({rec (R, A) ↾}_{ω}) (n), b \in ({rec (R, A) ↾}_{ω}) (n) ⟼ a \cap b) \subseteq fi (A)$
126	102 125	eqsstrd	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to ({rec (R, A) ↾}_{ω}) (suc n) \subseteq fi (A)$
127	117 126	jctild	$⊢ (n \in ω \land ({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A)) \to (\forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n) \to (({rec (R, A) ↾}_{ω}) (suc n) \subseteq fi (A) \land \forall y \in suc n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n)))$
128	127	expimpd	$⊢ n \in ω \to ((({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A) \land \forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n)) \to (({rec (R, A) ↾}_{ω}) (suc n) \subseteq fi (A) \land \forall y \in suc n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n)))$
129	128	a1d	$⊢ n \in ω \to (A \in V \to ((({rec (R, A) ↾}_{ω}) (n) \subseteq fi (A) \land \forall y \in n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (n)) \to (({rec (R, A) ↾}_{ω}) (suc n) \subseteq fi (A) \land \forall y \in suc n ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (suc n))))$
130	37 42 47 49 129	finds2	$⊢ x \in ω \to (A \in V \to (({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \land \forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)))$
131	130	impcom	$⊢ (A \in V \land x \in ω) \to (({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A) \land \forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x))$
132	131	simprd	$⊢ (A \in V \land x \in ω) \to \forall y \in x ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)$
133	132	r19.21bi	$⊢ ((A \in V \land x \in ω) \land y \in x) \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)$
134	133	ex	$⊢ (A \in V \land x \in ω) \to (y \in x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x))$
135	134	adantr	$⊢ ((A \in V \land x \in ω) \land y \in ω) \to (y \in x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x))$
136		fveq2	$⊢ y = x \to ({rec (R, A) ↾}_{ω}) (y) = ({rec (R, A) ↾}_{ω}) (x)$
137		eqimss	$⊢ ({rec (R, A) ↾}_{ω}) (y) = ({rec (R, A) ↾}_{ω}) (x) \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)$
138	136 137	syl	$⊢ y = x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)$
139	138	a1i	$⊢ ((A \in V \land x \in ω) \land y \in ω) \to (y = x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x))$
140	135 139	jaod	$⊢ ((A \in V \land x \in ω) \land y \in ω) \to ((y \in x \lor y = x) \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x))$
141	32 140	sylbid	$⊢ ((A \in V \land x \in ω) \land y \in ω) \to (y \subseteq x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x))$
142	141	ralrimiva	$⊢ (A \in V \land x \in ω) \to \forall y \in ω (y \subseteq x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x))$
143	142	ralrimiva	$⊢ A \in V \to \forall x \in ω \forall y \in ω (y \subseteq x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x))$
144	143	adantr	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to \forall x \in ω \forall y \in ω (y \subseteq x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x))$
145		ssun1	$⊢ m \subseteq m \cup n$
146	145	a1i	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to m \subseteq m \cup n$
147		sseq2	$⊢ x = m \cup n \to (y \subseteq x \leftrightarrow y \subseteq m \cup n)$
148		fveq2	$⊢ x = m \cup n \to ({rec (R, A) ↾}_{ω}) (x) = ({rec (R, A) ↾}_{ω}) (m \cup n)$
149	148	sseq2d	$⊢ x = m \cup n \to (({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x) \leftrightarrow ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n))$
150	147 149	imbi12d	$⊢ x = m \cup n \to ((y \subseteq x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)) \leftrightarrow (y \subseteq m \cup n \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n)))$
151		sseq1	$⊢ y = m \to (y \subseteq m \cup n \leftrightarrow m \subseteq m \cup n)$
152		fveq2	$⊢ y = m \to ({rec (R, A) ↾}_{ω}) (y) = ({rec (R, A) ↾}_{ω}) (m)$
153	152	sseq1d	$⊢ y = m \to (({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n) \leftrightarrow ({rec (R, A) ↾}_{ω}) (m) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n))$
154	151 153	imbi12d	$⊢ y = m \to ((y \subseteq m \cup n \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n)) \leftrightarrow (m \subseteq m \cup n \to ({rec (R, A) ↾}_{ω}) (m) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n)))$
155	150 154	rspc2v	$⊢ (m \cup n \in ω \land m \in ω) \to (\forall x \in ω \forall y \in ω (y \subseteq x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)) \to (m \subseteq m \cup n \to ({rec (R, A) ↾}_{ω}) (m) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n)))$
156	27 144 146 155	syl3c	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to ({rec (R, A) ↾}_{ω}) (m) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n)$
157	156	sseld	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to (c \in ({rec (R, A) ↾}_{ω}) (m) \to c \in ({rec (R, A) ↾}_{ω}) (m \cup n))$
158		simprr	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to n \in ω$
159	25 158	jca	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to (m \cup n \in ω \land n \in ω)$
160		ssun2	$⊢ n \subseteq m \cup n$
161	160	a1i	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to n \subseteq m \cup n$
162		sseq1	$⊢ y = n \to (y \subseteq m \cup n \leftrightarrow n \subseteq m \cup n)$
163	108	sseq1d	$⊢ y = n \to (({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n) \leftrightarrow ({rec (R, A) ↾}_{ω}) (n) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n))$
164	162 163	imbi12d	$⊢ y = n \to ((y \subseteq m \cup n \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n)) \leftrightarrow (n \subseteq m \cup n \to ({rec (R, A) ↾}_{ω}) (n) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n)))$
165	150 164	rspc2v	$⊢ (m \cup n \in ω \land n \in ω) \to (\forall x \in ω \forall y \in ω (y \subseteq x \to ({rec (R, A) ↾}_{ω}) (y) \subseteq ({rec (R, A) ↾}_{ω}) (x)) \to (n \subseteq m \cup n \to ({rec (R, A) ↾}_{ω}) (n) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n)))$
166	159 144 161 165	syl3c	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to ({rec (R, A) ↾}_{ω}) (n) \subseteq ({rec (R, A) ↾}_{ω}) (m \cup n)$
167	166	sseld	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to (d \in ({rec (R, A) ↾}_{ω}) (n) \to d \in ({rec (R, A) ↾}_{ω}) (m \cup n))$
168	24	ad2antlr	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to m \cup n \in ω$
169		peano2	$⊢ m \cup n \in ω \to suc (m \cup n) \in ω$
170		fveq2	$⊢ x = suc (m \cup n) \to ({rec (R, A) ↾}_{ω}) (x) = ({rec (R, A) ↾}_{ω}) (suc (m \cup n))$
171	170	ssiun2s	$⊢ suc (m \cup n) \in ω \to ({rec (R, A) ↾}_{ω}) (suc (m \cup n)) \subseteq ⋃_{x \in ω} ({rec (R, A) ↾}_{ω}) (x)$
172	168 169 171	3syl	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to ({rec (R, A) ↾}_{ω}) (suc (m \cup n)) \subseteq ⋃_{x \in ω} ({rec (R, A) ↾}_{ω}) (x)$
173		simprl	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to c \in ({rec (R, A) ↾}_{ω}) (m \cup n)$
174		simprr	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to d \in ({rec (R, A) ↾}_{ω}) (m \cup n)$
175		eqidd	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to c \cap d = c \cap d$
176		ineq1	$⊢ a = c \to a \cap b = c \cap b$
177	176	eqeq2d	$⊢ a = c \to (c \cap d = a \cap b \leftrightarrow c \cap d = c \cap b)$
178		ineq2	$⊢ b = d \to c \cap b = c \cap d$
179	178	eqeq2d	$⊢ b = d \to (c \cap d = c \cap b \leftrightarrow c \cap d = c \cap d)$
180	177 179	rspc2ev	$⊢ (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land c \cap d = c \cap d) \to \exists a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \exists b \in ({rec (R, A) ↾}_{ω}) (m \cup n) c \cap d = a \cap b$
181	173 174 175 180	syl3anc	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to \exists a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \exists b \in ({rec (R, A) ↾}_{ω}) (m \cup n) c \cap d = a \cap b$
182		vex	$⊢ c \in V$
183	182	inex1	$⊢ c \cap d \in V$
184		eqeq1	$⊢ x = c \cap d \to (x = a \cap b \leftrightarrow c \cap d = a \cap b)$
185	184	2rexbidv	$⊢ x = c \cap d \to (\exists a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \exists b \in ({rec (R, A) ↾}_{ω}) (m \cup n) x = a \cap b \leftrightarrow \exists a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \exists b \in ({rec (R, A) ↾}_{ω}) (m \cup n) c \cap d = a \cap b)$
186	183 185	elab	$⊢ c \cap d \in \{x \| \exists a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \exists b \in ({rec (R, A) ↾}_{ω}) (m \cup n) x = a \cap b\} \leftrightarrow \exists a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \exists b \in ({rec (R, A) ↾}_{ω}) (m \cup n) c \cap d = a \cap b$
187	181 186	sylibr	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to c \cap d \in \{x \| \exists a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \exists b \in ({rec (R, A) ↾}_{ω}) (m \cup n) x = a \cap b\}$
188		eqid	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b) = (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b)$
189	188	rnmpo	$⊢ ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b) = \{x \| \exists a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \exists b \in ({rec (R, A) ↾}_{ω}) (m \cup n) x = a \cap b\}$
190	187 189	eleqtrrdi	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to c \cap d \in ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b)$
191		fvex	$⊢ ({rec (R, A) ↾}_{ω}) (m \cup n) \in V$
192	191	uniex	$⊢ ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n) \in V$
193	192	pwex	$⊢ 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n) \in V$
194		elssuni	$⊢ a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \to a \subseteq ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
195	69 194	sstrid	$⊢ a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \to a \cap b \subseteq ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
196	74	elpw	$⊢ a \cap b \in 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n) \leftrightarrow a \cap b \subseteq ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
197	195 196	sylibr	$⊢ a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \to a \cap b \in 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
198	197	adantr	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land b \in ({rec (R, A) ↾}_{ω}) (m \cup n)) \to a \cap b \in 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
199	198	rgen2	$⊢ \forall a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \forall b \in ({rec (R, A) ↾}_{ω}) (m \cup n) a \cap b \in 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
200	188	fmpo	$⊢ \forall a \in ({rec (R, A) ↾}_{ω}) (m \cup n) \forall b \in ({rec (R, A) ↾}_{ω}) (m \cup n) a \cap b \in 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n) \leftrightarrow (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b) : ({rec (R, A) ↾}_{ω}) (m \cup n) \times ({rec (R, A) ↾}_{ω}) (m \cup n) ⟶ 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
201	199 200	mpbi	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b) : ({rec (R, A) ↾}_{ω}) (m \cup n) \times ({rec (R, A) ↾}_{ω}) (m \cup n) ⟶ 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
202		frn	$⊢ (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b) : ({rec (R, A) ↾}_{ω}) (m \cup n) \times ({rec (R, A) ↾}_{ω}) (m \cup n) ⟶ 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n) \to ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b) \subseteq 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
203	201 202	ax-mp	$⊢ ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b) \subseteq 𝒫 ⋃ ({rec (R, A) ↾}_{ω}) (m \cup n)$
204	193 203	ssexi	$⊢ ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b) \in V$
205		nfcv	$⊢ \underline{Ⅎ} v (m \cup n)$
206		nfcv	$⊢ \underline{Ⅎ} v ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b)$
207		mpoeq12	$⊢ (v = ({rec (R, A) ↾}_{ω}) (m \cup n) \land v = ({rec (R, A) ↾}_{ω}) (m \cup n)) \to (a \in v, b \in v ⟼ a \cap b) = (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b)$
208	207	anidms	$⊢ v = ({rec (R, A) ↾}_{ω}) (m \cup n) \to (a \in v, b \in v ⟼ a \cap b) = (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b)$
209	208	rneqd	$⊢ v = ({rec (R, A) ↾}_{ω}) (m \cup n) \to ran (a \in v, b \in v ⟼ a \cap b) = ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b)$
210	83 205 206 97 209	frsucmpt	$⊢ (m \cup n \in ω \land ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b) \in V) \to ({rec (R, A) ↾}_{ω}) (suc (m \cup n)) = ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b)$
211	168 204 210	sylancl	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to ({rec (R, A) ↾}_{ω}) (suc (m \cup n)) = ran (a \in ({rec (R, A) ↾}_{ω}) (m \cup n), b \in ({rec (R, A) ↾}_{ω}) (m \cup n) ⟼ a \cap b)$
212	190 211	eleqtrrd	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to c \cap d \in ({rec (R, A) ↾}_{ω}) (suc (m \cup n))$
213	172 212	sseldd	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to c \cap d \in ⋃_{x \in ω} ({rec (R, A) ↾}_{ω}) (x)$
214		fniunfv	$⊢ ({rec (R, A) ↾}_{ω}) Fn ω \to ⋃_{x \in ω} ({rec (R, A) ↾}_{ω}) (x) = ⋃ ran ({rec (R, A) ↾}_{ω})$
215	4 214	ax-mp	$⊢ ⋃_{x \in ω} ({rec (R, A) ↾}_{ω}) (x) = ⋃ ran ({rec (R, A) ↾}_{ω})$
216	213 215	eleqtrdi	$⊢ ((A \in V \land (m \in ω \land n \in ω)) \land (c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n))) \to c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω})$
217	216	ex	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to ((c \in ({rec (R, A) ↾}_{ω}) (m \cup n) \land d \in ({rec (R, A) ↾}_{ω}) (m \cup n)) \to c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
218	157 167 217	syl2and	$⊢ (A \in V \land (m \in ω \land n \in ω)) \to ((c \in ({rec (R, A) ↾}_{ω}) (m) \land d \in ({rec (R, A) ↾}_{ω}) (n)) \to c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
219	218	rexlimdvva	$⊢ A \in V \to (\exists m \in ω \exists n \in ω (c \in ({rec (R, A) ↾}_{ω}) (m) \land d \in ({rec (R, A) ↾}_{ω}) (n)) \to c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
220	219	imp	$⊢ (A \in V \land \exists m \in ω \exists n \in ω (c \in ({rec (R, A) ↾}_{ω}) (m) \land d \in ({rec (R, A) ↾}_{ω}) (n))) \to c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω})$
221	21 220	sylan2br	$⊢ (A \in V \land (c \in ⋃ ran ({rec (R, A) ↾}_{ω}) \land d \in ⋃ ran ({rec (R, A) ↾}_{ω}))) \to c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω})$
222	221	ralrimivva	$⊢ A \in V \to \forall c \in ⋃ ran ({rec (R, A) ↾}_{ω}) \forall d \in ⋃ ran ({rec (R, A) ↾}_{ω}) c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω})$
223	131	simpld	$⊢ (A \in V \land x \in ω) \to ({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A)$
224		fvex	$⊢ fi (A) \in V$
225	224	elpw2	$⊢ ({rec (R, A) ↾}_{ω}) (x) \in 𝒫 fi (A) \leftrightarrow ({rec (R, A) ↾}_{ω}) (x) \subseteq fi (A)$
226	223 225	sylibr	$⊢ (A \in V \land x \in ω) \to ({rec (R, A) ↾}_{ω}) (x) \in 𝒫 fi (A)$
227	226	ralrimiva	$⊢ A \in V \to \forall x \in ω ({rec (R, A) ↾}_{ω}) (x) \in 𝒫 fi (A)$
228		fnfvrnss	$⊢ (({rec (R, A) ↾}_{ω}) Fn ω \land \forall x \in ω ({rec (R, A) ↾}_{ω}) (x) \in 𝒫 fi (A)) \to ran ({rec (R, A) ↾}_{ω}) \subseteq 𝒫 fi (A)$
229	4 227 228	sylancr	$⊢ A \in V \to ran ({rec (R, A) ↾}_{ω}) \subseteq 𝒫 fi (A)$
230		sspwuni	$⊢ ran ({rec (R, A) ↾}_{ω}) \subseteq 𝒫 fi (A) \leftrightarrow ⋃ ran ({rec (R, A) ↾}_{ω}) \subseteq fi (A)$
231	229 230	sylib	$⊢ A \in V \to ⋃ ran ({rec (R, A) ↾}_{ω}) \subseteq fi (A)$
232		ssexg	$⊢ (⋃ ran ({rec (R, A) ↾}_{ω}) \subseteq fi (A) \land fi (A) \in V) \to ⋃ ran ({rec (R, A) ↾}_{ω}) \in V$
233	231 224 232	sylancl	$⊢ A \in V \to ⋃ ran ({rec (R, A) ↾}_{ω}) \in V$
234		sseq2	$⊢ x = ⋃ ran ({rec (R, A) ↾}_{ω}) \to (A \subseteq x \leftrightarrow A \subseteq ⋃ ran ({rec (R, A) ↾}_{ω}))$
235		eleq2	$⊢ x = ⋃ ran ({rec (R, A) ↾}_{ω}) \to (c \cap d \in x \leftrightarrow c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
236	235	raleqbi1dv	$⊢ x = ⋃ ran ({rec (R, A) ↾}_{ω}) \to (\forall d \in x c \cap d \in x \leftrightarrow \forall d \in ⋃ ran ({rec (R, A) ↾}_{ω}) c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
237	236	raleqbi1dv	$⊢ x = ⋃ ran ({rec (R, A) ↾}_{ω}) \to (\forall c \in x \forall d \in x c \cap d \in x \leftrightarrow \forall c \in ⋃ ran ({rec (R, A) ↾}_{ω}) \forall d \in ⋃ ran ({rec (R, A) ↾}_{ω}) c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω}))$
238	234 237	anbi12d	$⊢ x = ⋃ ran ({rec (R, A) ↾}_{ω}) \to ((A \subseteq x \land \forall c \in x \forall d \in x c \cap d \in x) \leftrightarrow (A \subseteq ⋃ ran ({rec (R, A) ↾}_{ω}) \land \forall c \in ⋃ ran ({rec (R, A) ↾}_{ω}) \forall d \in ⋃ ran ({rec (R, A) ↾}_{ω}) c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω})))$
239	238	elabg	$⊢ ⋃ ran ({rec (R, A) ↾}_{ω}) \in V \to (⋃ ran ({rec (R, A) ↾}_{ω}) \in \{x \| (A \subseteq x \land \forall c \in x \forall d \in x c \cap d \in x)\} \leftrightarrow (A \subseteq ⋃ ran ({rec (R, A) ↾}_{ω}) \land \forall c \in ⋃ ran ({rec (R, A) ↾}_{ω}) \forall d \in ⋃ ran ({rec (R, A) ↾}_{ω}) c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω})))$
240	233 239	syl	$⊢ A \in V \to (⋃ ran ({rec (R, A) ↾}_{ω}) \in \{x \| (A \subseteq x \land \forall c \in x \forall d \in x c \cap d \in x)\} \leftrightarrow (A \subseteq ⋃ ran ({rec (R, A) ↾}_{ω}) \land \forall c \in ⋃ ran ({rec (R, A) ↾}_{ω}) \forall d \in ⋃ ran ({rec (R, A) ↾}_{ω}) c \cap d \in ⋃ ran ({rec (R, A) ↾}_{ω})))$
241	10 222 240	mpbir2and	$⊢ A \in V \to ⋃ ran ({rec (R, A) ↾}_{ω}) \in \{x \| (A \subseteq x \land \forall c \in x \forall d \in x c \cap d \in x)\}$
242		intss1	$⊢ ⋃ ran ({rec (R, A) ↾}_{ω}) \in \{x \| (A \subseteq x \land \forall c \in x \forall d \in x c \cap d \in x)\} \to ⋂ \{x \| (A \subseteq x \land \forall c \in x \forall d \in x c \cap d \in x)\} \subseteq ⋃ ran ({rec (R, A) ↾}_{ω})$
243	241 242	syl	$⊢ A \in V \to ⋂ \{x \| (A \subseteq x \land \forall c \in x \forall d \in x c \cap d \in x)\} \subseteq ⋃ ran ({rec (R, A) ↾}_{ω})$
244	2 243	eqsstrd	$⊢ A \in V \to fi (A) \subseteq ⋃ ran ({rec (R, A) ↾}_{ω})$
245	244 231	eqssd	$⊢ A \in V \to fi (A) = ⋃ ran ({rec (R, A) ↾}_{ω})$
246		df-ima	$⊢ rec (R, A) [ω] = ran ({rec (R, A) ↾}_{ω})$
247	246	unieqi	$⊢ ⋃ rec (R, A) [ω] = ⋃ ran ({rec (R, A) ↾}_{ω})$
248	245 247	eqtr4di	$⊢ A \in V \to fi (A) = ⋃ rec (R, A) [ω]$

Metamath Proof Explorer

Theorem dffi3

Proof