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