Metamath Proof Explorer

Theorem isf32lem1

Description: Lemma for isfin3-2 . Derive weak ordering property. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Hypotheses isf32lem.a ⊢ φ → F : ω ⟶ 𝒫 G
isf32lem.b ⊢ φ → ∀ x ∈ ω F ⁡ suc ⁡ x ⊆ F ⁡ x
isf32lem.c ⊢ φ → ¬ ⋂ ran ⁡ F ∈ ran ⁡ F
Assertion isf32lem1 ⊢ A ∈ ω ∧ B ∈ ω ∧ B ⊆ A ∧ φ → F ⁡ A ⊆ F ⁡ B

Proof

Step Hyp Ref Expression
1 isf32lem.a ⊢ φ → F : ω ⟶ 𝒫 G
2 isf32lem.b ⊢ φ → ∀ x ∈ ω F ⁡ suc ⁡ x ⊆ F ⁡ x
3 isf32lem.c ⊢ φ → ¬ ⋂ ran ⁡ F ∈ ran ⁡ F
4 fveq2 ⊢ a = B → F ⁡ a = F ⁡ B
5 4 sseq1d ⊢ a = B → F ⁡ a ⊆ F ⁡ B ↔ F ⁡ B ⊆ F ⁡ B
6 5 imbi2d ⊢ a = B → φ → F ⁡ a ⊆ F ⁡ B ↔ φ → F ⁡ B ⊆ F ⁡ B
7 fveq2 ⊢ a = b → F ⁡ a = F ⁡ b
8 7 sseq1d ⊢ a = b → F ⁡ a ⊆ F ⁡ B ↔ F ⁡ b ⊆ F ⁡ B
9 8 imbi2d ⊢ a = b → φ → F ⁡ a ⊆ F ⁡ B ↔ φ → F ⁡ b ⊆ F ⁡ B
10 fveq2 ⊢ a = suc ⁡ b → F ⁡ a = F ⁡ suc ⁡ b
11 10 sseq1d ⊢ a = suc ⁡ b → F ⁡ a ⊆ F ⁡ B ↔ F ⁡ suc ⁡ b ⊆ F ⁡ B
12 11 imbi2d ⊢ a = suc ⁡ b → φ → F ⁡ a ⊆ F ⁡ B ↔ φ → F ⁡ suc ⁡ b ⊆ F ⁡ B
13 fveq2 ⊢ a = A → F ⁡ a = F ⁡ A
14 13 sseq1d ⊢ a = A → F ⁡ a ⊆ F ⁡ B ↔ F ⁡ A ⊆ F ⁡ B
15 14 imbi2d ⊢ a = A → φ → F ⁡ a ⊆ F ⁡ B ↔ φ → F ⁡ A ⊆ F ⁡ B
16 ssid ⊢ F ⁡ B ⊆ F ⁡ B
17 16 2a1i ⊢ B ∈ ω → φ → F ⁡ B ⊆ F ⁡ B
18 suceq ⊢ x = b → suc ⁡ x = suc ⁡ b
19 18 fveq2d ⊢ x = b → F ⁡ suc ⁡ x = F ⁡ suc ⁡ b
20 fveq2 ⊢ x = b → F ⁡ x = F ⁡ b
21 19 20 sseq12d ⊢ x = b → F ⁡ suc ⁡ x ⊆ F ⁡ x ↔ F ⁡ suc ⁡ b ⊆ F ⁡ b
22 21 rspcv ⊢ b ∈ ω → ∀ x ∈ ω F ⁡ suc ⁡ x ⊆ F ⁡ x → F ⁡ suc ⁡ b ⊆ F ⁡ b
23 2 22 syl5 ⊢ b ∈ ω → φ → F ⁡ suc ⁡ b ⊆ F ⁡ b
24 23 ad2antrr ⊢ b ∈ ω ∧ B ∈ ω ∧ B ⊆ b → φ → F ⁡ suc ⁡ b ⊆ F ⁡ b
25 sstr2 ⊢ F ⁡ suc ⁡ b ⊆ F ⁡ b → F ⁡ b ⊆ F ⁡ B → F ⁡ suc ⁡ b ⊆ F ⁡ B
26 24 25 syl6 ⊢ b ∈ ω ∧ B ∈ ω ∧ B ⊆ b → φ → F ⁡ b ⊆ F ⁡ B → F ⁡ suc ⁡ b ⊆ F ⁡ B
27 26 a2d ⊢ b ∈ ω ∧ B ∈ ω ∧ B ⊆ b → φ → F ⁡ b ⊆ F ⁡ B → φ → F ⁡ suc ⁡ b ⊆ F ⁡ B
28 6 9 12 15 17 27 findsg ⊢ A ∈ ω ∧ B ∈ ω ∧ B ⊆ A → φ → F ⁡ A ⊆ F ⁡ B
29 28 impr ⊢ A ∈ ω ∧ B ∈ ω ∧ B ⊆ A ∧ φ → F ⁡ A ⊆ F ⁡ B