Theorem canthwe

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

	Ref	Expression
Hypothesis	canthwe.1	⊢ 𝑂 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) }
Assertion	canthwe	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≺ 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		canthwe.1	⊢ 𝑂 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) }
2		simp1	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ⊆ 𝐴 )
3		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
4	2 3	sylibr	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ∈ 𝒫 𝐴 )
5		simp2	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑟 ⊆ ( 𝑥 × 𝑥 ) )
6		xpss12	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 × 𝑥 ) ⊆ ( 𝐴 × 𝐴 ) )
7	2 2 6	syl2anc	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ( 𝑥 × 𝑥 ) ⊆ ( 𝐴 × 𝐴 ) )
8	5 7	sstrd	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑟 ⊆ ( 𝐴 × 𝐴 ) )
9		velpw	⊢ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ↔ 𝑟 ⊆ ( 𝐴 × 𝐴 ) )
10	8 9	sylibr	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) )
11	4 10	jca	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) )
12	11	ssopab2i	⊢ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ⊆ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) }
13		df-xp	⊢ ( 𝒫 𝐴 × 𝒫 ( 𝐴 × 𝐴 ) ) = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) }
14	12 1 13	3sstr4i	⊢ 𝑂 ⊆ ( 𝒫 𝐴 × 𝒫 ( 𝐴 × 𝐴 ) )
15		pwexg	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
16		sqxpexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × 𝐴 ) ∈ V )
17	16	pwexd	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 ( 𝐴 × 𝐴 ) ∈ V )
18	15 17	xpexd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 × 𝒫 ( 𝐴 × 𝐴 ) ) ∈ V )
19		ssexg	⊢ ( ( 𝑂 ⊆ ( 𝒫 𝐴 × 𝒫 ( 𝐴 × 𝐴 ) ) ∧ ( 𝒫 𝐴 × 𝒫 ( 𝐴 × 𝐴 ) ) ∈ V ) → 𝑂 ∈ V )
20	14 18 19	sylancr	⊢ ( 𝐴 ∈ 𝑉 → 𝑂 ∈ V )
21		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ 𝐴 )
22	21	snssd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴 ) → { 𝑢 } ⊆ 𝐴 )
23		0ss	⊢ ∅ ⊆ ( { 𝑢 } × { 𝑢 } )
24	23	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴 ) → ∅ ⊆ ( { 𝑢 } × { 𝑢 } ) )
25		rel0	⊢ Rel ∅
26		br0	⊢ ¬ 𝑢 ∅ 𝑢
27		wesn	⊢ ( Rel ∅ → ( ∅ We { 𝑢 } ↔ ¬ 𝑢 ∅ 𝑢 ) )
28	26 27	mpbiri	⊢ ( Rel ∅ → ∅ We { 𝑢 } )
29	25 28	mp1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴 ) → ∅ We { 𝑢 } )
30		vsnex	⊢ { 𝑢 } ∈ V
31		0ex	⊢ ∅ ∈ V
32		simpl	⊢ ( ( 𝑥 = { 𝑢 } ∧ 𝑟 = ∅ ) → 𝑥 = { 𝑢 } )
33	32	sseq1d	⊢ ( ( 𝑥 = { 𝑢 } ∧ 𝑟 = ∅ ) → ( 𝑥 ⊆ 𝐴 ↔ { 𝑢 } ⊆ 𝐴 ) )
34		simpr	⊢ ( ( 𝑥 = { 𝑢 } ∧ 𝑟 = ∅ ) → 𝑟 = ∅ )
35	32	sqxpeqd	⊢ ( ( 𝑥 = { 𝑢 } ∧ 𝑟 = ∅ ) → ( 𝑥 × 𝑥 ) = ( { 𝑢 } × { 𝑢 } ) )
36	34 35	sseq12d	⊢ ( ( 𝑥 = { 𝑢 } ∧ 𝑟 = ∅ ) → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ ∅ ⊆ ( { 𝑢 } × { 𝑢 } ) ) )
37	34 32	weeq12d	⊢ ( ( 𝑥 = { 𝑢 } ∧ 𝑟 = ∅ ) → ( 𝑟 We 𝑥 ↔ ∅ We { 𝑢 } ) )
38	33 36 37	3anbi123d	⊢ ( ( 𝑥 = { 𝑢 } ∧ 𝑟 = ∅ ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ↔ ( { 𝑢 } ⊆ 𝐴 ∧ ∅ ⊆ ( { 𝑢 } × { 𝑢 } ) ∧ ∅ We { 𝑢 } ) ) )
39	30 31 38	opelopaba	⊢ ( ⟨ { 𝑢 } , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ↔ ( { 𝑢 } ⊆ 𝐴 ∧ ∅ ⊆ ( { 𝑢 } × { 𝑢 } ) ∧ ∅ We { 𝑢 } ) )
40	22 24 29 39	syl3anbrc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴 ) → ⟨ { 𝑢 } , ∅ ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } )
41	40 1	eleqtrrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴 ) → ⟨ { 𝑢 } , ∅ ⟩ ∈ 𝑂 )
42	41	ex	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑢 ∈ 𝐴 → ⟨ { 𝑢 } , ∅ ⟩ ∈ 𝑂 ) )
43		eqid	⊢ ∅ = ∅
44		vsnex	⊢ { 𝑣 } ∈ V
45	44 31	opth2	⊢ ( ⟨ { 𝑢 } , ∅ ⟩ = ⟨ { 𝑣 } , ∅ ⟩ ↔ ( { 𝑢 } = { 𝑣 } ∧ ∅ = ∅ ) )
46	43 45	mpbiran2	⊢ ( ⟨ { 𝑢 } , ∅ ⟩ = ⟨ { 𝑣 } , ∅ ⟩ ↔ { 𝑢 } = { 𝑣 } )
47		sneqbg	⊢ ( 𝑢 ∈ V → ( { 𝑢 } = { 𝑣 } ↔ 𝑢 = 𝑣 ) )
48	47	elv	⊢ ( { 𝑢 } = { 𝑣 } ↔ 𝑢 = 𝑣 )
49	46 48	bitri	⊢ ( ⟨ { 𝑢 } , ∅ ⟩ = ⟨ { 𝑣 } , ∅ ⟩ ↔ 𝑢 = 𝑣 )
50	49	2a1i	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( ⟨ { 𝑢 } , ∅ ⟩ = ⟨ { 𝑣 } , ∅ ⟩ ↔ 𝑢 = 𝑣 ) ) )
51	42 50	dom2d	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑂 ∈ V → 𝐴 ≼ 𝑂 ) )
52	20 51	mpd	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≼ 𝑂 )
53		eqid	⊢ { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) }
54	53	fpwwe2cbv	⊢ { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑤 ] ( 𝑤 𝑓 ( 𝑟 ∩ ( 𝑤 × 𝑤 ) ) ) = 𝑦 ) ) }
55		eqid	⊢ ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } = ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) }
56		eqid	⊢ ( ◡ ( { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } ‘ ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } ) “ { ( ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } 𝑓 ( { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } ‘ ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } ) ) } ) = ( ◡ ( { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } ‘ ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } ) “ { ( ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } 𝑓 ( { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } ‘ ∪ dom { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝑓 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) } ) ) } )
57	1 54 55 56	canthwelem	⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝑓 : 𝑂 –1-1→ 𝐴 )
58		f1of1	⊢ ( 𝑓 : 𝑂 –1-1-onto→ 𝐴 → 𝑓 : 𝑂 –1-1→ 𝐴 )
59	57 58	nsyl	⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝑓 : 𝑂 –1-1-onto→ 𝐴 )
60	59	nexdv	⊢ ( 𝐴 ∈ 𝑉 → ¬ ∃ 𝑓 𝑓 : 𝑂 –1-1-onto→ 𝐴 )
61		ensym	⊢ ( 𝐴 ≈ 𝑂 → 𝑂 ≈ 𝐴 )
62		bren	⊢ ( 𝑂 ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 𝑂 –1-1-onto→ 𝐴 )
63	61 62	sylib	⊢ ( 𝐴 ≈ 𝑂 → ∃ 𝑓 𝑓 : 𝑂 –1-1-onto→ 𝐴 )
64	60 63	nsyl	⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝐴 ≈ 𝑂 )
65		brsdom	⊢ ( 𝐴 ≺ 𝑂 ↔ ( 𝐴 ≼ 𝑂 ∧ ¬ 𝐴 ≈ 𝑂 ) )
66	52 64 65	sylanbrc	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≺ 𝑂 )