Metamath Proof Explorer

Theorem isf32lem12

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

		Ref	Expression
	Hypothesis	isf32lem40.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
	Assertion	isf32lem12	$⊢ G \in V \to (\neg ω ≼^{*} G \to G \in F)$

Proof

Step	Hyp	Ref	Expression
1		isf32lem40.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
2		elmapi	$⊢ f \in ({𝒫 G}^{ω}) \to f : ω ⟶ 𝒫 G$
3		isf32lem11	$⊢ (G \in V \land (f : ω ⟶ 𝒫 G \land \forall b \in ω f (suc b) \subseteq f (b) \land \neg ⋂ ran f \in ran f)) \to ω ≼^{*} G$
4	3	expcom	$⊢ (f : ω ⟶ 𝒫 G \land \forall b \in ω f (suc b) \subseteq f (b) \land \neg ⋂ ran f \in ran f) \to (G \in V \to ω ≼^{*} G)$
5	4	3expa	$⊢ ((f : ω ⟶ 𝒫 G \land \forall b \in ω f (suc b) \subseteq f (b)) \land \neg ⋂ ran f \in ran f) \to (G \in V \to ω ≼^{*} G)$
6	5	impancom	$⊢ ((f : ω ⟶ 𝒫 G \land \forall b \in ω f (suc b) \subseteq f (b)) \land G \in V) \to (\neg ⋂ ran f \in ran f \to ω ≼^{*} G)$
7	6	con1d	$⊢ ((f : ω ⟶ 𝒫 G \land \forall b \in ω f (suc b) \subseteq f (b)) \land G \in V) \to (\neg ω ≼^{*} G \to ⋂ ran f \in ran f)$
8	7	exp31	$⊢ f : ω ⟶ 𝒫 G \to (\forall b \in ω f (suc b) \subseteq f (b) \to (G \in V \to (\neg ω ≼^{*} G \to ⋂ ran f \in ran f)))$
9	2 8	syl	$⊢ f \in ({𝒫 G}^{ω}) \to (\forall b \in ω f (suc b) \subseteq f (b) \to (G \in V \to (\neg ω ≼^{*} G \to ⋂ ran f \in ran f)))$
10	9	com4t	$⊢ G \in V \to (\neg ω ≼^{*} G \to (f \in ({𝒫 G}^{ω}) \to (\forall b \in ω f (suc b) \subseteq f (b) \to ⋂ ran f \in ran f)))$
11	10	ralrimdv	$⊢ G \in V \to (\neg ω ≼^{*} G \to \forall f \in ({𝒫 G}^{ω}) (\forall b \in ω f (suc b) \subseteq f (b) \to ⋂ ran f \in ran f))$
12	1	isfin3ds	$⊢ G \in V \to (G \in F \leftrightarrow \forall f \in ({𝒫 G}^{ω}) (\forall b \in ω f (suc b) \subseteq f (b) \to ⋂ ran f \in ran f))$
13	11 12	sylibrd	$⊢ G \in V \to (\neg ω ≼^{*} G \to G \in F)$