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 ) )