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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≺ 𝑂 )