Metamath Proof Explorer

Theorem infxpenc2lem1

Description: Lemma for infxpenc2 . (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses infxpenc2.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
infxpenc2.2 ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
infxpenc2.3 ⊢ 𝑊 = ( ◡ ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) )
Assertion infxpenc2lem1 ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ( 𝑊 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 infxpenc2.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
2 infxpenc2.2 ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
3 infxpenc2.3 ⊢ 𝑊 = ( ◡ ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) )
4 2 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
5 4 impr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) )
6 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
7 oveq2 ⊢ ( 𝑥 = 𝑤 → ( ω ↑o 𝑥 ) = ( ω ↑o 𝑤 ) )
8 eqid ⊢ ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) = ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) )
9 ovex ⊢ ( ω ↑o 𝑤 ) ∈ V
10 7 8 9 fvmpt ⊢ ( 𝑤 ∈ ( On ∖ 1o ) → ( ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ 𝑤 ) = ( ω ↑o 𝑤 ) )
11 10 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ 𝑤 ) = ( ω ↑o 𝑤 ) )
12 f1ofo ⊢ ( ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) → ( 𝑛 ‘ 𝑏 ) : 𝑏 –onto→ ( ω ↑o 𝑤 ) )
13 12 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( 𝑛 ‘ 𝑏 ) : 𝑏 –onto→ ( ω ↑o 𝑤 ) )
14 forn ⊢ ( ( 𝑛 ‘ 𝑏 ) : 𝑏 –onto→ ( ω ↑o 𝑤 ) → ran ( 𝑛 ‘ 𝑏 ) = ( ω ↑o 𝑤 ) )
15 13 14 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ran ( 𝑛 ‘ 𝑏 ) = ( ω ↑o 𝑤 ) )
16 11 15 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ 𝑤 ) = ran ( 𝑛 ‘ 𝑏 ) )
17 ovex ⊢ ( ω ↑o 𝑥 ) ∈ V
18 17 2a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( 𝑥 ∈ ( On ∖ 1o ) → ( ω ↑o 𝑥 ) ∈ V ) )
19 omelon ⊢ ω ∈ On
20 1onn ⊢ 1o ∈ ω
21 ondif2 ⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
22 19 20 21 mpbir2an ⊢ ω ∈ ( On ∖ 2o )
23 eldifi ⊢ ( 𝑥 ∈ ( On ∖ 1o ) → 𝑥 ∈ On )
24 23 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) ∧ ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝑦 ∈ ( On ∖ 1o ) ) ) → 𝑥 ∈ On )
25 eldifi ⊢ ( 𝑦 ∈ ( On ∖ 1o ) → 𝑦 ∈ On )
26 25 ad2antll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) ∧ ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝑦 ∈ ( On ∖ 1o ) ) ) → 𝑦 ∈ On )
27 oecan ⊢ ( ( ω ∈ ( On ∖ 2o ) ∧ 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( ω ↑o 𝑥 ) = ( ω ↑o 𝑦 ) ↔ 𝑥 = 𝑦 ) )
28 22 24 26 27 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) ∧ ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝑦 ∈ ( On ∖ 1o ) ) ) → ( ( ω ↑o 𝑥 ) = ( ω ↑o 𝑦 ) ↔ 𝑥 = 𝑦 ) )
29 28 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝑦 ∈ ( On ∖ 1o ) ) → ( ( ω ↑o 𝑥 ) = ( ω ↑o 𝑦 ) ↔ 𝑥 = 𝑦 ) ) )
30 18 29 dom2lem ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) : ( On ∖ 1o ) –1-1→ V )
31 f1f1orn ⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) : ( On ∖ 1o ) –1-1→ V → ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) : ( On ∖ 1o ) –1-1-onto→ ran ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) )
32 30 31 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) : ( On ∖ 1o ) –1-1-onto→ ran ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) )
33 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → 𝑤 ∈ ( On ∖ 1o ) )
34 f1ocnvfv ⊢ ( ( ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) : ( On ∖ 1o ) –1-1-onto→ ran ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ∧ 𝑤 ∈ ( On ∖ 1o ) ) → ( ( ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ 𝑤 ) = ran ( 𝑛 ‘ 𝑏 ) → ( ◡ ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) ) = 𝑤 ) )
35 32 33 34 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( ( ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ 𝑤 ) = ran ( 𝑛 ‘ 𝑏 ) → ( ◡ ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) ) = 𝑤 ) )
36 16 35 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( ◡ ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) ) = 𝑤 )
37 3 36 syl5eq ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → 𝑊 = 𝑤 )
38 37 eleq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( 𝑊 ∈ ( On ∖ 1o ) ↔ 𝑤 ∈ ( On ∖ 1o ) ) )
39 37 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( ω ↑o 𝑊 ) = ( ω ↑o 𝑤 ) )
40 39 f1oeq3d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
41 38 40 anbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( ( 𝑊 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ) ↔ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) )
42 6 41 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) ∧ ( 𝑤 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) → ( 𝑊 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
43 5 42 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ( 𝑊 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ) )