This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
isf32lem.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
isf32lem.c ⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
Assertion isf32lem1 ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝜑 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 isf32lem.a ⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
2 isf32lem.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
3 isf32lem.c ⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
4 fveq2 ⊢ ( 𝑎 = 𝐵 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐵 ) )
5 4 sseq1d ⊢ ( 𝑎 = 𝐵 → ( ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
6 5 imbi2d ⊢ ( 𝑎 = 𝐵 → ( ( 𝜑 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ) )
7 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) )
8 7 sseq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
9 8 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝜑 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ) )
10 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ suc 𝑏 ) )
11 10 sseq1d ⊢ ( 𝑎 = suc 𝑏 → ( ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
12 11 imbi2d ⊢ ( 𝑎 = suc 𝑏 → ( ( 𝜑 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ) )
13 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐴 ) )
14 13 sseq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
15 14 imbi2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝜑 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ) )
16 ssid ⊢ ( 𝐹 ‘ 𝐵 ) ⊆ ( 𝐹 ‘ 𝐵 )
17 16 2a1i ⊢ ( 𝐵 ∈ ω → ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
18 suceq ⊢ ( 𝑥 = 𝑏 → suc 𝑥 = suc 𝑏 )
19 18 fveq2d ⊢ ( 𝑥 = 𝑏 → ( 𝐹 ‘ suc 𝑥 ) = ( 𝐹 ‘ suc 𝑏 ) )
20 fveq2 ⊢ ( 𝑥 = 𝑏 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑏 ) )
21 19 20 sseq12d ⊢ ( 𝑥 = 𝑏 → ( ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) )
22 21 rspcv ⊢ ( 𝑏 ∈ ω → ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) )
23 2 22 syl5 ⊢ ( 𝑏 ∈ ω → ( 𝜑 → ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) )
24 23 ad2antrr ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑏 ) → ( 𝜑 → ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) )
25 sstr2 ⊢ ( ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) → ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
26 24 25 syl6 ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑏 ) → ( 𝜑 → ( ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) → ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ) )
27 26 a2d ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑏 ) → ( ( 𝜑 → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) → ( 𝜑 → ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ) )
28 6 9 12 15 17 27 findsg ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
29 28 impr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝜑 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) )