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 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑m 𝑛 ) = ( 𝐴 ↑m 𝑘 ) )
9 8 cbviunv ⊢ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) = ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 )
10 f1eq3 ⊢ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) = ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) → ( 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↔ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ) )
11 9 10 ax-mp ⊢ ( 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↔ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) )
12 11 bilani ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) )
13 simpllr ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → 𝑡 ⊆ 𝐴 )
14 simplll ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ℎ : ω –1-1-onto→ 𝑡 )
15 biid ⊢ ( ( ( 𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑢 × 𝑢 ) ∧ 𝑟 We 𝑢 ) ∧ ω ≼ 𝑢 ) ↔ ( ( 𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑢 × 𝑢 ) ∧ 𝑟 We 𝑢 ) ∧ ω ≼ 𝑢 ) )
16 simplr ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
17 sseq2 ⊢ ( 𝑏 = 𝑤 → ( ω ⊆ 𝑏 ↔ ω ⊆ 𝑤 ) )
18 fveq2 ⊢ ( 𝑏 = 𝑤 → ( 𝑚 ‘ 𝑏 ) = ( 𝑚 ‘ 𝑤 ) )
19 18 f1oeq1d ⊢ ( 𝑏 = 𝑤 → ( ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑚 ‘ 𝑤 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
20 xpeq12 ⊢ ( ( 𝑏 = 𝑤 ∧ 𝑏 = 𝑤 ) → ( 𝑏 × 𝑏 ) = ( 𝑤 × 𝑤 ) )
21 20 anidms ⊢ ( 𝑏 = 𝑤 → ( 𝑏 × 𝑏 ) = ( 𝑤 × 𝑤 ) )
22 21 f1oeq2d ⊢ ( 𝑏 = 𝑤 → ( ( 𝑚 ‘ 𝑤 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑏 ) )
23 f1oeq3 ⊢ ( 𝑏 = 𝑤 → ( ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑏 ↔ ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) )
24 19 22 23 3bitrd ⊢ ( 𝑏 = 𝑤 → ( ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) )
25 17 24 imbi12d ⊢ ( 𝑏 = 𝑤 → ( ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ↔ ( ω ⊆ 𝑤 → ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) ) )
26 25 cbvralvw ⊢ ( ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ↔ ∀ 𝑤 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑤 → ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) )
27 16 26 sylib ⊢ ( ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ∀ 𝑤 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑤 → ( 𝑚 ‘ 𝑤 ) : ( 𝑤 × 𝑤 ) –1-1-onto→ 𝑤 ) )
28 eqid ⊢ OrdIso ( 𝑟 , 𝑢 ) = OrdIso ( 𝑟 , 𝑢 )
29 eqid ⊢ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) = ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ )
30 eqid ⊢ ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) ) = ( ( OrdIso ( 𝑟 , 𝑢 ) ∘ ( 𝑚 ‘ dom OrdIso ( 𝑟 , 𝑢 ) ) ) ∘ ◡ ( 𝑠 ∈ dom OrdIso ( 𝑟 , 𝑢 ) , 𝑧 ∈ dom OrdIso ( 𝑟 , 𝑢 ) ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑠 ) , ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑧 ) ⟩ ) )
31 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 ( 𝑟 , 𝑢 ) ‘ ∅ ) ⟩ } )
32 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑢 ↑m 𝑛 ) = ( 𝑢 ↑m 𝑘 ) )
33 32 cbviunv ⊢ ∪ 𝑛 ∈ ω ( 𝑢 ↑m 𝑛 ) = ∪ 𝑘 ∈ ω ( 𝑢 ↑m 𝑘 )
34 33 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 𝑦 ) ‘ 𝑦 ) ⟩ )
35 eqid ⊢ ( 𝑥 ∈ ω , 𝑦 ∈ 𝑢 ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑥 ) , 𝑦 ⟩ ) = ( 𝑥 ∈ ω , 𝑦 ∈ 𝑢 ↦ ⟨ ( OrdIso ( 𝑟 , 𝑢 ) ‘ 𝑥 ) , 𝑦 ⟩ )
36 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 𝑦 ) ‘ 𝑦 ) ⟩ ) )
37 12 13 14 15 27 28 29 30 31 34 35 36 pwfseqlem5 ⊢ ¬ ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ∧ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
38 37 imnani ⊢ ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) → ¬ 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
39 38 nexdv ⊢ ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) → ¬ ∃ 𝑔 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
40 brdomi ⊢ ( 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → ∃ 𝑔 𝑔 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
41 39 40 nsyl ⊢ ( ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) ∧ ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
42 41 ex ⊢ ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ( ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
43 42 exlimdv ⊢ ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ( ∃ 𝑚 ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑚 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
44 7 43 mpi ⊢ ( ( ℎ : ω –1-1-onto→ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
45 44 ex ⊢ ( ℎ : ω –1-1-onto→ 𝑡 → ( 𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
46 45 exlimiv ⊢ ( ∃ ℎ ℎ : ω –1-1-onto→ 𝑡 → ( 𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
47 4 46 sylbi ⊢ ( ω ≈ 𝑡 → ( 𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
48 47 imp ⊢ ( ( ω ≈ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
49 48 exlimiv ⊢ ( ∃ 𝑡 ( ω ≈ 𝑡 ∧ 𝑡 ⊆ 𝐴 ) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
50 3 49 biimtrdi ⊢ ( 𝐴 ∈ V → ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
51 2 50 mpcom ⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )