Metamath Proof Explorer

Theorem fin23lem35

Description: Lemma for fin23 . Strict order property of Y . (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem33.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
fin23lem.f ⊢ φ → h : ω ⟶ 1-1 V
fin23lem.g ⊢ φ → ⋃ ran ⁡ h ⊆ G
fin23lem.h ⊢ φ → ∀ j j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ j ⊆ G → i ⁡ j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ j ⊂ ⋃ ran ⁡ j
fin23lem.i ⊢ Y = rec ⁡ i h ↾ ω
Assertion fin23lem35 ⊢ φ ∧ A ∈ ω → ⋃ ran ⁡ Y ⁡ suc ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A

Proof

Step Hyp Ref Expression
1 fin23lem33.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
2 fin23lem.f ⊢ φ → h : ω ⟶ 1-1 V
3 fin23lem.g ⊢ φ → ⋃ ran ⁡ h ⊆ G
4 fin23lem.h ⊢ φ → ∀ j j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ j ⊆ G → i ⁡ j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ j ⊂ ⋃ ran ⁡ j
5 fin23lem.i ⊢ Y = rec ⁡ i h ↾ ω
6 1 2 3 4 5 fin23lem34 ⊢ φ ∧ A ∈ ω → Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ Y ⁡ A ⊆ G
7 fvex ⊢ Y ⁡ A ∈ V
8 f1eq1 ⊢ j = Y ⁡ A → j : ω ⟶ 1-1 V ↔ Y ⁡ A : ω ⟶ 1-1 V
9 rneq ⊢ j = Y ⁡ A → ran ⁡ j = ran ⁡ Y ⁡ A
10 9 unieqd ⊢ j = Y ⁡ A → ⋃ ran ⁡ j = ⋃ ran ⁡ Y ⁡ A
11 10 sseq1d ⊢ j = Y ⁡ A → ⋃ ran ⁡ j ⊆ G ↔ ⋃ ran ⁡ Y ⁡ A ⊆ G
12 8 11 anbi12d ⊢ j = Y ⁡ A → j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ j ⊆ G ↔ Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ Y ⁡ A ⊆ G
13 fveq2 ⊢ j = Y ⁡ A → i ⁡ j = i ⁡ Y ⁡ A
14 f1eq1 ⊢ i ⁡ j = i ⁡ Y ⁡ A → i ⁡ j : ω ⟶ 1-1 V ↔ i ⁡ Y ⁡ A : ω ⟶ 1-1 V
15 13 14 syl ⊢ j = Y ⁡ A → i ⁡ j : ω ⟶ 1-1 V ↔ i ⁡ Y ⁡ A : ω ⟶ 1-1 V
16 13 rneqd ⊢ j = Y ⁡ A → ran ⁡ i ⁡ j = ran ⁡ i ⁡ Y ⁡ A
17 16 unieqd ⊢ j = Y ⁡ A → ⋃ ran ⁡ i ⁡ j = ⋃ ran ⁡ i ⁡ Y ⁡ A
18 17 10 psseq12d ⊢ j = Y ⁡ A → ⋃ ran ⁡ i ⁡ j ⊂ ⋃ ran ⁡ j ↔ ⋃ ran ⁡ i ⁡ Y ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A
19 15 18 anbi12d ⊢ j = Y ⁡ A → i ⁡ j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ j ⊂ ⋃ ran ⁡ j ↔ i ⁡ Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ Y ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A
20 12 19 imbi12d ⊢ j = Y ⁡ A → j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ j ⊆ G → i ⁡ j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ j ⊂ ⋃ ran ⁡ j ↔ Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ Y ⁡ A ⊆ G → i ⁡ Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ Y ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A
21 7 20 spcv ⊢ ∀ j j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ j ⊆ G → i ⁡ j : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ j ⊂ ⋃ ran ⁡ j → Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ Y ⁡ A ⊆ G → i ⁡ Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ Y ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A
22 4 21 syl ⊢ φ → Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ Y ⁡ A ⊆ G → i ⁡ Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ Y ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A
23 22 adantr ⊢ φ ∧ A ∈ ω → Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ Y ⁡ A ⊆ G → i ⁡ Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ Y ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A
24 6 23 mpd ⊢ φ ∧ A ∈ ω → i ⁡ Y ⁡ A : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ i ⁡ Y ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A
25 24 simprd ⊢ φ ∧ A ∈ ω → ⋃ ran ⁡ i ⁡ Y ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A
26 frsuc ⊢ A ∈ ω → rec ⁡ i h ↾ ω ⁡ suc ⁡ A = i ⁡ rec ⁡ i h ↾ ω ⁡ A
27 26 adantl ⊢ φ ∧ A ∈ ω → rec ⁡ i h ↾ ω ⁡ suc ⁡ A = i ⁡ rec ⁡ i h ↾ ω ⁡ A
28 5 fveq1i ⊢ Y ⁡ suc ⁡ A = rec ⁡ i h ↾ ω ⁡ suc ⁡ A
29 5 fveq1i ⊢ Y ⁡ A = rec ⁡ i h ↾ ω ⁡ A
30 29 fveq2i ⊢ i ⁡ Y ⁡ A = i ⁡ rec ⁡ i h ↾ ω ⁡ A
31 27 28 30 3eqtr4g ⊢ φ ∧ A ∈ ω → Y ⁡ suc ⁡ A = i ⁡ Y ⁡ A
32 31 rneqd ⊢ φ ∧ A ∈ ω → ran ⁡ Y ⁡ suc ⁡ A = ran ⁡ i ⁡ Y ⁡ A
33 32 unieqd ⊢ φ ∧ A ∈ ω → ⋃ ran ⁡ Y ⁡ suc ⁡ A = ⋃ ran ⁡ i ⁡ Y ⁡ A
34 33 psseq1d ⊢ φ ∧ A ∈ ω → ⋃ ran ⁡ Y ⁡ suc ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A ↔ ⋃ ran ⁡ i ⁡ Y ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A
35 25 34 mpbird ⊢ φ ∧ A ∈ ω → ⋃ ran ⁡ Y ⁡ suc ⁡ A ⊂ ⋃ ran ⁡ Y ⁡ A