Metamath Proof Explorer

Theorem tz9.1c

Description: Alternate expression for the existence of transitive closures tz9.1 : the intersection of all transitive sets containing A is a set. (Contributed by Mario Carneiro, 22-Mar-2013)

		Ref	Expression
	Hypothesis	tz9.1.1	$⊢ A \in V$
	Assertion	tz9.1c	$⊢ ⋂ \{x \| (A \subseteq x \land Tr x)\} \in V$

Proof

Step	Hyp	Ref	Expression
1		tz9.1.1	$⊢ A \in V$
2		eqid	$⊢ {rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω} = {rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}$
3		eqid	$⊢ ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) = ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w)$
4	1 2 3	trcl	$⊢ (A \subseteq ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \land Tr ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \land \forall x ((A \subseteq x \land Tr x) \to ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \subseteq x))$
5		3simpa	$⊢ (A \subseteq ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \land Tr ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \land \forall x ((A \subseteq x \land Tr x) \to ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \subseteq x)) \to (A \subseteq ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \land Tr ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w))$
6		omex	$⊢ ω \in V$
7		fvex	$⊢ ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \in V$
8	6 7	iunex	$⊢ ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \in V$
9		sseq2	$⊢ x = ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \to (A \subseteq x \leftrightarrow A \subseteq ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w))$
10		treq	$⊢ x = ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \to (Tr x \leftrightarrow Tr ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w))$
11	9 10	anbi12d	$⊢ x = ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \to ((A \subseteq x \land Tr x) \leftrightarrow (A \subseteq ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \land Tr ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w)))$
12	8 11	spcev	$⊢ (A \subseteq ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w) \land Tr ⋃_{w \in ω} ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (w)) \to \exists x (A \subseteq x \land Tr x)$
13	4 5 12	mp2b	$⊢ \exists x (A \subseteq x \land Tr x)$
14		abn0	$⊢ \{x \| (A \subseteq x \land Tr x)\} \neq \emptyset \leftrightarrow \exists x (A \subseteq x \land Tr x)$
15	13 14	mpbir	$⊢ \{x \| (A \subseteq x \land Tr x)\} \neq \emptyset$
16		intex	$⊢ \{x \| (A \subseteq x \land Tr x)\} \neq \emptyset \leftrightarrow ⋂ \{x \| (A \subseteq x \land Tr x)\} \in V$
17	15 16	mpbi	$⊢ ⋂ \{x \| (A \subseteq x \land Tr x)\} \in V$