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

Metamath Proof Explorer

Theorem domssex

Description: Weakening of domssex2 to forget the functions in favor of dominance and equinumerosity. (Contributed by Mario Carneiro, 7-Feb-2015) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion domssex ( 𝐴 ≼ 𝐵 → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 brdomi ⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
2 reldom ⊢ Rel ≼
3 2 brrelex2i ⊢ ( 𝐴 ≼ 𝐵 → 𝐵 ∈ V )
4 vex ⊢ 𝑓 ∈ V
5 f1stres ⊢ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ⟶ ( 𝐵 ∖ ran 𝑓 )
6 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ ran 𝑓 ) ∈ V )
7 6 adantl ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐵 ∖ ran 𝑓 ) ∈ V )
8 snex ⊢ { 𝒫 ∪ ran 𝐴 } ∈ V
9 xpexg ⊢ ( ( ( 𝐵 ∖ ran 𝑓 ) ∈ V ∧ { 𝒫 ∪ ran 𝐴 } ∈ V ) → ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ∈ V )
10 7 8 9 sylancl ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ∈ V )
11 fex2 ⊢ ( ( ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ⟶ ( 𝐵 ∖ ran 𝑓 ) ∧ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ∈ V ∧ ( 𝐵 ∖ ran 𝑓 ) ∈ V ) → ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ∈ V )
12 5 10 7 11 mp3an2i ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ∈ V )
13 unexg ⊢ ( ( 𝑓 ∈ V ∧ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ∈ V ) → ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
14 4 12 13 sylancr ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
15 cnvexg ⊢ ( ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V → ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
16 14 15 syl ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
17 rnexg ⊢ ( ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V → ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
18 16 17 syl ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V )
19 simpl ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → 𝑓 : 𝐴 –1-1→ 𝐵 )
20 f1dm ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → dom 𝑓 = 𝐴 )
21 4 dmex ⊢ dom 𝑓 ∈ V
22 20 21 eqeltrrdi ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝐴 ∈ V )
23 22 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
24 simpr ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
25 eqid ⊢ ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) = ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) )
26 25 domss2 ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ 𝐴 ⊆ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ ( ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝑓 ) = ( I ↾ 𝐴 ) ) )
27 19 23 24 26 syl3anc ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ( ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ 𝐴 ⊆ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ ( ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∘ 𝑓 ) = ( I ↾ 𝐴 ) ) )
28 27 simp2d ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ⊆ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
29 27 simp1d ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
30 f1oen3g ⊢ ( ( ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∈ V ∧ ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ) → 𝐵 ≈ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
31 16 29 30 syl2anc ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → 𝐵 ≈ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) )
32 28 31 jca ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ( 𝐴 ⊆ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ 𝐵 ≈ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ) )
33 sseq2 ⊢ ( 𝑥 = ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ) )
34 breq2 ⊢ ( 𝑥 = ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 𝐵 ≈ 𝑥 ↔ 𝐵 ≈ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ) )
35 33 34 anbi12d ⊢ ( 𝑥 = ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( ( 𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥 ) ↔ ( 𝐴 ⊆ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ∧ 𝐵 ≈ ran ◡ ( 𝑓 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝑓 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ) ) )
36 18 32 35 spcedv ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥 ) )
37 36 ex ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ( 𝐵 ∈ V → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥 ) ) )
38 37 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 → ( 𝐵 ∈ V → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥 ) ) )
39 1 3 38 sylc ⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥 ) )