tz9.12lem3

Description: Lemma for tz9.12 . (Contributed by NM, 22-Sep-2003) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	tz9.12lem.1	$⊢ A \in V$
	tz9.12lem.2	$⊢ F = (z \in V ⟼ ⋂ \{v \in On \| z \in R_{1} (v)\})$
Assertion	tz9.12lem3	$⊢ \forall x \in A \exists y \in On x \in R_{1} (y) \to A \in R_{1} (suc suc ⋃ F [A])$

Proof

Step	Hyp	Ref	Expression
1		tz9.12lem.1	$⊢ A \in V$
2		tz9.12lem.2	$⊢ F = (z \in V ⟼ ⋂ \{v \in On \| z \in R_{1} (v)\})$
3	2	funmpt2	$⊢ Fun F$
4		fveq2	$⊢ v = y \to R_{1} (v) = R_{1} (y)$
5	4	eleq2d	$⊢ v = y \to (x \in R_{1} (v) \leftrightarrow x \in R_{1} (y))$
6	5	rspcev	$⊢ (y \in On \land x \in R_{1} (y)) \to \exists v \in On x \in R_{1} (v)$
7		rabn0	$⊢ \{v \in On \| x \in R_{1} (v)\} \neq \emptyset \leftrightarrow \exists v \in On x \in R_{1} (v)$
8	6 7	sylibr	$⊢ (y \in On \land x \in R_{1} (y)) \to \{v \in On \| x \in R_{1} (v)\} \neq \emptyset$
9		intex	$⊢ \{v \in On \| x \in R_{1} (v)\} \neq \emptyset \leftrightarrow ⋂ \{v \in On \| x \in R_{1} (v)\} \in V$
10	8 9	sylib	$⊢ (y \in On \land x \in R_{1} (y)) \to ⋂ \{v \in On \| x \in R_{1} (v)\} \in V$
11		vex	$⊢ x \in V$
12		eleq1w	$⊢ z = x \to (z \in R_{1} (v) \leftrightarrow x \in R_{1} (v))$
13	12	rabbidv	$⊢ z = x \to \{v \in On \| z \in R_{1} (v)\} = \{v \in On \| x \in R_{1} (v)\}$
14	13	inteqd	$⊢ z = x \to ⋂ \{v \in On \| z \in R_{1} (v)\} = ⋂ \{v \in On \| x \in R_{1} (v)\}$
15	14	eleq1d	$⊢ z = x \to (⋂ \{v \in On \| z \in R_{1} (v)\} \in V \leftrightarrow ⋂ \{v \in On \| x \in R_{1} (v)\} \in V)$
16	2	dmmpt	$⊢ dom F = \{z \in V \| ⋂ \{v \in On \| z \in R_{1} (v)\} \in V\}$
17	15 16	elrab2	$⊢ x \in dom F \leftrightarrow (x \in V \land ⋂ \{v \in On \| x \in R_{1} (v)\} \in V)$
18	11 17	mpbiran	$⊢ x \in dom F \leftrightarrow ⋂ \{v \in On \| x \in R_{1} (v)\} \in V$
19	10 18	sylibr	$⊢ (y \in On \land x \in R_{1} (y)) \to x \in dom F$
20		funfvima	$⊢ (Fun F \land x \in dom F) \to (x \in A \to F (x) \in F [A])$
21	3 19 20	sylancr	$⊢ (y \in On \land x \in R_{1} (y)) \to (x \in A \to F (x) \in F [A])$
22	1 2	tz9.12lem2	$⊢ suc ⋃ F [A] \in On$
23	1 2	tz9.12lem1	$⊢ F [A] \subseteq On$
24		onsucuni	$⊢ F [A] \subseteq On \to F [A] \subseteq suc ⋃ F [A]$
25	23 24	ax-mp	$⊢ F [A] \subseteq suc ⋃ F [A]$
26	25	sseli	$⊢ F (x) \in F [A] \to F (x) \in suc ⋃ F [A]$
27		r1ord2	$⊢ suc ⋃ F [A] \in On \to (F (x) \in suc ⋃ F [A] \to R_{1} (F (x)) \subseteq R_{1} (suc ⋃ F [A]))$
28	22 26 27	mpsyl	$⊢ F (x) \in F [A] \to R_{1} (F (x)) \subseteq R_{1} (suc ⋃ F [A])$
29	21 28	syl6	$⊢ (y \in On \land x \in R_{1} (y)) \to (x \in A \to R_{1} (F (x)) \subseteq R_{1} (suc ⋃ F [A]))$
30	29	imp	$⊢ ((y \in On \land x \in R_{1} (y)) \land x \in A) \to R_{1} (F (x)) \subseteq R_{1} (suc ⋃ F [A])$
31	14 2	fvmptg	$⊢ (x \in V \land ⋂ \{v \in On \| x \in R_{1} (v)\} \in V) \to F (x) = ⋂ \{v \in On \| x \in R_{1} (v)\}$
32	11 31	mpan	$⊢ ⋂ \{v \in On \| x \in R_{1} (v)\} \in V \to F (x) = ⋂ \{v \in On \| x \in R_{1} (v)\}$
33	9 32	sylbi	$⊢ \{v \in On \| x \in R_{1} (v)\} \neq \emptyset \to F (x) = ⋂ \{v \in On \| x \in R_{1} (v)\}$
34		ssrab2	$⊢ \{v \in On \| x \in R_{1} (v)\} \subseteq On$
35		onint	$⊢ (\{v \in On \| x \in R_{1} (v)\} \subseteq On \land \{v \in On \| x \in R_{1} (v)\} \neq \emptyset) \to ⋂ \{v \in On \| x \in R_{1} (v)\} \in \{v \in On \| x \in R_{1} (v)\}$
36	34 35	mpan	$⊢ \{v \in On \| x \in R_{1} (v)\} \neq \emptyset \to ⋂ \{v \in On \| x \in R_{1} (v)\} \in \{v \in On \| x \in R_{1} (v)\}$
37	33 36	eqeltrd	$⊢ \{v \in On \| x \in R_{1} (v)\} \neq \emptyset \to F (x) \in \{v \in On \| x \in R_{1} (v)\}$
38		fveq2	$⊢ y = F (x) \to R_{1} (y) = R_{1} (F (x))$
39	38	eleq2d	$⊢ y = F (x) \to (x \in R_{1} (y) \leftrightarrow x \in R_{1} (F (x)))$
40	5	cbvrabv	$⊢ \{v \in On \| x \in R_{1} (v)\} = \{y \in On \| x \in R_{1} (y)\}$
41	39 40	elrab2	$⊢ F (x) \in \{v \in On \| x \in R_{1} (v)\} \leftrightarrow (F (x) \in On \land x \in R_{1} (F (x)))$
42	41	simprbi	$⊢ F (x) \in \{v \in On \| x \in R_{1} (v)\} \to x \in R_{1} (F (x))$
43	8 37 42	3syl	$⊢ (y \in On \land x \in R_{1} (y)) \to x \in R_{1} (F (x))$
44	43	adantr	$⊢ ((y \in On \land x \in R_{1} (y)) \land x \in A) \to x \in R_{1} (F (x))$
45	30 44	sseldd	$⊢ ((y \in On \land x \in R_{1} (y)) \land x \in A) \to x \in R_{1} (suc ⋃ F [A])$
46	45	exp31	$⊢ y \in On \to (x \in R_{1} (y) \to (x \in A \to x \in R_{1} (suc ⋃ F [A])))$
47	46	com3r	$⊢ x \in A \to (y \in On \to (x \in R_{1} (y) \to x \in R_{1} (suc ⋃ F [A])))$
48	47	rexlimdv	$⊢ x \in A \to (\exists y \in On x \in R_{1} (y) \to x \in R_{1} (suc ⋃ F [A]))$
49	48	ralimia	$⊢ \forall x \in A \exists y \in On x \in R_{1} (y) \to \forall x \in A x \in R_{1} (suc ⋃ F [A])$
50		r1suc	$⊢ suc ⋃ F [A] \in On \to R_{1} (suc suc ⋃ F [A]) = 𝒫 R_{1} (suc ⋃ F [A])$
51	22 50	ax-mp	$⊢ R_{1} (suc suc ⋃ F [A]) = 𝒫 R_{1} (suc ⋃ F [A])$
52	51	eleq2i	$⊢ A \in R_{1} (suc suc ⋃ F [A]) \leftrightarrow A \in 𝒫 R_{1} (suc ⋃ F [A])$
53	1	elpw	$⊢ A \in 𝒫 R_{1} (suc ⋃ F [A]) \leftrightarrow A \subseteq R_{1} (suc ⋃ F [A])$
54		dfss3	$⊢ A \subseteq R_{1} (suc ⋃ F [A]) \leftrightarrow \forall x \in A x \in R_{1} (suc ⋃ F [A])$
55	52 53 54	3bitri	$⊢ A \in R_{1} (suc suc ⋃ F [A]) \leftrightarrow \forall x \in A x \in R_{1} (suc ⋃ F [A])$
56	49 55	sylibr	$⊢ \forall x \in A \exists y \in On x \in R_{1} (y) \to A \in R_{1} (suc suc ⋃ F [A])$

Metamath Proof Explorer

Theorem tz9.12lem3

Proof