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 ( 𝐴𝐵 → ∃ 𝑥 ( 𝐴𝑥𝐵𝑥 ) )