This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem canthnum

Description: The set of well-orderable subsets of a set A strictly dominates A . A stronger form of canth2 . Corollary 1.4(a) of KanamoriPincus p. 417. (Contributed by Mario Carneiro, 19-May-2015)

Ref Expression
Assertion canthnum ( 𝐴 ∈ 𝑉 → 𝐴 ≺ ( 𝒫 𝐴 ∩ dom card ) )

Proof

Step Hyp Ref Expression
1 pwexg ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
2 inex1g ⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
3 infpwfidom ⊢ ( ( 𝒫 𝐴 ∩ Fin ) ∈ V → 𝐴 ≼ ( 𝒫 𝐴 ∩ Fin ) )
4 1 2 3 3syl ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≼ ( 𝒫 𝐴 ∩ Fin ) )
5 inex1g ⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∩ dom card ) ∈ V )
6 1 5 syl ⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 ∩ dom card ) ∈ V )
7 finnum ⊢ ( 𝑥 ∈ Fin → 𝑥 ∈ dom card )
8 7 ssriv ⊢ Fin ⊆ dom card
9 sslin ⊢ ( Fin ⊆ dom card → ( 𝒫 𝐴 ∩ Fin ) ⊆ ( 𝒫 𝐴 ∩ dom card ) )
10 8 9 ax-mp ⊢ ( 𝒫 𝐴 ∩ Fin ) ⊆ ( 𝒫 𝐴 ∩ dom card )
11 ssdomg ⊢ ( ( 𝒫 𝐴 ∩ dom card ) ∈ V → ( ( 𝒫 𝐴 ∩ Fin ) ⊆ ( 𝒫 𝐴 ∩ dom card ) → ( 𝒫 𝐴 ∩ Fin ) ≼ ( 𝒫 𝐴 ∩ dom card ) ) )
12 6 10 11 mpisyl ⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 ∩ Fin ) ≼ ( 𝒫 𝐴 ∩ dom card ) )
13 domtr ⊢ ( ( 𝐴 ≼ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝒫 𝐴 ∩ Fin ) ≼ ( 𝒫 𝐴 ∩ dom card ) ) → 𝐴 ≼ ( 𝒫 𝐴 ∩ dom card ) )
14 4 12 13 syl2anc ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≼ ( 𝒫 𝐴 ∩ dom card ) )
15 eqid ⊢ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
16 15 fpwwecbv ⊢ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑓 ‘ ( ◡ 𝑠 “ { 𝑧 } ) ) = 𝑧 ) ) }
17 eqid ⊢ ∪ dom { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } = ∪ dom { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
18 eqid ⊢ ( ◡ ( { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } ‘ ∪ dom { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } ) “ { ( 𝑓 ‘ ∪ dom { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } ) } ) = ( ◡ ( { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } ‘ ∪ dom { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } ) “ { ( 𝑓 ‘ ∪ dom { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } ) } )
19 16 17 18 canthnumlem ⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝑓 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 )
20 f1of1 ⊢ ( 𝑓 : ( 𝒫 𝐴 ∩ dom card ) –1-1-onto→ 𝐴 → 𝑓 : ( 𝒫 𝐴 ∩ dom card ) –1-1→ 𝐴 )
21 19 20 nsyl ⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝑓 : ( 𝒫 𝐴 ∩ dom card ) –1-1-onto→ 𝐴 )
22 21 nexdv ⊢ ( 𝐴 ∈ 𝑉 → ¬ ∃ 𝑓 𝑓 : ( 𝒫 𝐴 ∩ dom card ) –1-1-onto→ 𝐴 )
23 ensym ⊢ ( 𝐴 ≈ ( 𝒫 𝐴 ∩ dom card ) → ( 𝒫 𝐴 ∩ dom card ) ≈ 𝐴 )
24 bren ⊢ ( ( 𝒫 𝐴 ∩ dom card ) ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ( 𝒫 𝐴 ∩ dom card ) –1-1-onto→ 𝐴 )
25 23 24 sylib ⊢ ( 𝐴 ≈ ( 𝒫 𝐴 ∩ dom card ) → ∃ 𝑓 𝑓 : ( 𝒫 𝐴 ∩ dom card ) –1-1-onto→ 𝐴 )
26 22 25 nsyl ⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝐴 ≈ ( 𝒫 𝐴 ∩ dom card ) )
27 brsdom ⊢ ( 𝐴 ≺ ( 𝒫 𝐴 ∩ dom card ) ↔ ( 𝐴 ≼ ( 𝒫 𝐴 ∩ dom card ) ∧ ¬ 𝐴 ≈ ( 𝒫 𝐴 ∩ dom card ) ) )
28 14 26 27 sylanbrc ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≺ ( 𝒫 𝐴 ∩ dom card ) )