Metamath Proof Explorer

Theorem pwfseq

Description: The powerset of a Dedekind-infinite set does not inject into the set of finite sequences. The proof is due to Halbeisen and Shelah. Proposition 1.7 of KanamoriPincus p. 418. (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion pwfseq ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )

Proof

Step Hyp Ref Expression
1 reldom ⊢ Rel ≼
2 1 brrelex2i ⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
3 domeng ⊢ ( 𝐴 ∈ V → ( ω ≼ 𝐴 ↔ ∃ 𝑡 ( ω ≈ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ) )
4 bren ⊢ ( ω ≈ 𝑡 ↔ ∃ ℎ ℎ : ω –1-1-onto→ 𝑡 )
5 harcl ⊢ ( har ‘ 𝒫 𝐴 ) ∈ On
6 infxpenc2 ⊢ ( ( har ‘ 𝒫 𝐴 ) ∈ On → ∃ 𝑚 ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
7 5 6 ax-mp ⊢ ∃ 𝑚 ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 )
8 simpr ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
9 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑m 𝑛 ) = ( 𝐴 ↑m 𝑘 ) )
10 9 cbviunv ⊢ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) = ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 )
11 f1eq3 ⊢ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) = ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) → ( 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↔ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ) )
12 10 11 ax-mp ⊢ ( 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↔ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) )
13 8 12 sylib ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) )
14 simpllr ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → 𝑡 ⊆ 𝐴 )
15 simplll ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ℎ : ω –1-1-onto→ 𝑡 )
16 biid ⊢ ( ( ( 𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑢 × 𝑢 ) ∧ 𝑟 We 𝑢 ) ∧ ω ≼ 𝑢 ) ↔ ( ( 𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑢 × 𝑢 ) ∧ 𝑟 We 𝑢 ) ∧ ω ≼ 𝑢 ) )
17 simplr ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
18 sseq2 ⊢ ( 𝑏 = 𝑤 → ( ω ⊆ 𝑏 ↔ ω ⊆ 𝑤 ) )
19 fveq2 ⊢ ( 𝑏 = 𝑤 → ( 𝑚 ‘ 𝑏 ) = ( 𝑚 ‘ 𝑤 ) )
20 f1oeq1 ⊢ ( ( 𝑚 ‘ 𝑏 ) = ( 𝑚 ‘ 𝑤 ) → ( ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑚 ‘ 𝑤 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
21 19 20 syl ⊢ ( 𝑏 = 𝑤 → ( ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑚 ‘ 𝑤 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
22 xpeq12 ⊢ ( ( 𝑏 = 𝑤 ∧ 𝑏 = 𝑤 ) → ( 𝑏 × 𝑏 ) = ( 𝑤 × 𝑤 ) )
23 22 anidms ⊢ ( 𝑏 = 𝑤 → ( 𝑏 × 𝑏 ) = ( 𝑤 × 𝑤 ) )
24 23 f1oeq2d ⊢ ( 𝑏 = 𝑤 → ( ( 𝑚 ‘ 𝑤 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑏 ) )
25 f1oeq3 ⊢ ( 𝑏 = 𝑤 → ( ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑏 ↔ ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) )
26 21 24 25 3bitrd ⊢ ( 𝑏 = 𝑤 → ( ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) )
27 18 26 imbi12d ⊢ ( 𝑏 = 𝑤 → ( ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ↔ ( ω ⊆ 𝑤 → ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) ) )
28 27 cbvralvw ⊢ ( ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ↔ ∀ 𝑤 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑤 → ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) )
29 17 28 sylib ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ∀ 𝑤 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑤 → ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) )
30 eqid ⊢ OrdIso ( 𝑟 , 𝑢 ) = OrdIso ( 𝑟 , 𝑢 )
31 eqid ⊢ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) = ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ )
32 eqid ⊢ ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) = ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) )
33 eqid ⊢ seqω ( ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝑢 ↑m suc 𝑝 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑝 ) ) ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) ( 𝑥 ‘ 𝑝 ) ) ) ) , { ⟨ ∅ , ( OrdIso ( 𝑟 , 𝑢 ) ‘ ∅ ) ⟩ } ) = seqω ( ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝑢 ↑m suc 𝑝 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑝 ) ) ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) ( 𝑥 ‘ 𝑝 ) ) ) ) , { ⟨ ∅ , ( OrdIso ( 𝑟 , 𝑢 ) ‘ ∅ ) ⟩ } )
34 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑢 ↑m 𝑛 ) = ( 𝑢 ↑m 𝑘 ) )
35 34 cbviunv ⊢ ∪ 𝑛 ∈ ω ( 𝑢 ↑m 𝑛 ) = ∪ 𝑘 ∈ ω ( 𝑢 ↑m 𝑘 )
36 35 mpteq1i ⊢ ( 𝑦 ∈ ∪ 𝑛 ∈ ω ( 𝑢 ↑m 𝑛 ) ↦ ⟨ dom 𝑦 , ( ( seqω ( ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝑢 ↑m suc 𝑝 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑝 ) ) ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) ( 𝑥 ‘ 𝑝 ) ) ) ) , { ⟨ ∅ , ( OrdIso ( 𝑟 , 𝑢 ) ‘ ∅ ) ⟩ } ) ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ ) = ( 𝑦 ∈ ∪ 𝑘 ∈ ω ( 𝑢 ↑m 𝑘 ) ↦ ⟨ dom 𝑦 , ( ( seqω ( ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝑢 ↑m suc 𝑝 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑝 ) ) ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) ( 𝑥 ‘ 𝑝 ) ) ) ) , { ⟨ ∅ , ( OrdIso ( 𝑟 , 𝑢 ) ‘ ∅ ) ⟩ } ) ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ )
37 eqid ⊢ ( 𝑥 ∈ ω , 𝑦 ∈ 𝑢 ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑥 ) , 𝑦 ⟩ ) = ( 𝑥 ∈ ω , 𝑦 ∈ 𝑢 ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑥 ) , 𝑦 ⟩ )
38 eqid ⊢ ( ( ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) ∘ ( 𝑥 ∈ ω , 𝑦 ∈ 𝑢 ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑥 ) , 𝑦 ⟩ ) ) ∘ ( 𝑦 ∈ ∪ 𝑛 ∈ ω ( 𝑢 ↑m 𝑛 ) ↦ ⟨ dom 𝑦 , ( ( seqω ( ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝑢 ↑m suc 𝑝 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑝 ) ) ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) ( 𝑥 ‘ 𝑝 ) ) ) ) , { ⟨ ∅ , ( OrdIso ( 𝑟 , 𝑢 ) ‘ ∅ ) ⟩ } ) ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ ) ) = ( ( ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) ∘ ( 𝑥 ∈ ω , 𝑦 ∈ 𝑢 ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑥 ) , 𝑦 ⟩ ) ) ∘ ( 𝑦 ∈ ∪ 𝑛 ∈ ω ( 𝑢 ↑m 𝑛 ) ↦ ⟨ dom 𝑦 , ( ( seqω ( ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝑢 ↑m suc 𝑝 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑝 ) ) ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) ( 𝑥 ‘ 𝑝 ) ) ) ) , { ⟨ ∅ , ( OrdIso ( 𝑟 , 𝑢 ) ‘ ∅ ) ⟩ } ) ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ ) )
39 13 14 15 16 29 30 31 32 33 36 37 38 pwfseqlem5 ⊢ ¬ ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
40 39 imnani ⊢ ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) → ¬ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
41 40 nexdv ⊢ ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) → ¬ ∃ 𝑔 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
42 brdomi ⊢ ( 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → ∃ 𝑔 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
43 41 42 nsyl ⊢ ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
44 43 ex ⊢ ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ( ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
45 44 exlimdv ⊢ ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ( ∃ 𝑚 ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
46 7 45 mpi ⊢ ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
47 46 ex ⊢ ( ℎ : ω –1-1-onto→ 𝑡 → ( 𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
48 47 exlimiv ⊢ ( ∃ ℎ ℎ : ω –1-1-onto→ 𝑡 → ( 𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
49 4 48 sylbi ⊢ ( ω ≈ 𝑡 → ( 𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
50 49 imp ⊢ ( ( ω ≈ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
51 50 exlimiv ⊢ ( ∃ 𝑡 ( ω ≈ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
52 3 51 syl6bi ⊢ ( 𝐴 ∈ V → ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
53 2 52 mpcom ⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )