Metamath Proof Explorer

Theorem isf32lem10

Description: Lemma for isfin3-2 . Write in terms of weak dominance. (Contributed by Stefan O'Rear, 6-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Hypotheses	isf32lem.a	$⊢ φ \to F : ω ⟶ 𝒫 G$
		isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
		isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
		isf32lem.d	$⊢ S = \{y \in ω \| F (suc y) \subset F (y)\}$
		isf32lem.e	$⊢ J = (u \in ω ⟼ (ι v \in S \| (v \cap S) \approx u))$
		isf32lem.f	$⊢ K = (w \in S ⟼ F (w) ∖ F (suc w)) \circ J$
		isf32lem.g	$⊢ L = (t \in G ⟼ (ι s \| (s \in ω \land t \in K (s))))$
	Assertion	isf32lem10	$⊢ φ \to (G \in V \to ω ≼^{*} G)$

Proof

Step	Hyp	Ref	Expression
1		isf32lem.a	$⊢ φ \to F : ω ⟶ 𝒫 G$
2		isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
3		isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
4		isf32lem.d	$⊢ S = \{y \in ω \| F (suc y) \subset F (y)\}$
5		isf32lem.e	$⊢ J = (u \in ω ⟼ (ι v \in S \| (v \cap S) \approx u))$
6		isf32lem.f	$⊢ K = (w \in S ⟼ F (w) ∖ F (suc w)) \circ J$
7		isf32lem.g	$⊢ L = (t \in G ⟼ (ι s \| (s \in ω \land t \in K (s))))$
8	1 2 3 4 5 6 7	isf32lem9	$⊢ φ \to L : G \underset{onto}{⟶} ω$
9		fof	$⊢ L : G \underset{onto}{⟶} ω \to L : G ⟶ ω$
10	8 9	syl	$⊢ φ \to L : G ⟶ ω$
11		fex	$⊢ (L : G ⟶ ω \land G \in V) \to L \in V$
12	10 11	sylan	$⊢ (φ \land G \in V) \to L \in V$
13	12	ex	$⊢ φ \to (G \in V \to L \in V)$
14		fowdom	$⊢ (L \in V \land L : G \underset{onto}{⟶} ω) \to ω ≼^{*} G$
15	14	expcom	$⊢ L : G \underset{onto}{⟶} ω \to (L \in V \to ω ≼^{*} G)$
16	8 13 15	sylsyld	$⊢ φ \to (G \in V \to ω ≼^{*} G)$