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	$⊢ A ≼ B \to \exists x (A \subseteq x \land B \approx x)$

Proof

Step	Hyp	Ref	Expression
1		brdomi	$⊢ A ≼ B \to \exists f f : A \underset{1-1}{⟶} B$
2		reldom	$⊢ Rel ≼$
3	2	brrelex2i	$⊢ A ≼ B \to B \in V$
4		vex	$⊢ f \in V$
5		f1stres	$⊢ ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}) : (B ∖ ran f) \times \{𝒫 ⋃ ran A\} ⟶ B ∖ ran f$
6		difexg	$⊢ B \in V \to B ∖ ran f \in V$
7	6	adantl	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to B ∖ ran f \in V$
8		snex	$⊢ \{𝒫 ⋃ ran A\} \in V$
9		xpexg	$⊢ (B ∖ ran f \in V \land \{𝒫 ⋃ ran A\} \in V) \to (B ∖ ran f) \times \{𝒫 ⋃ ran A\} \in V$
10	7 8 9	sylancl	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to (B ∖ ran f) \times \{𝒫 ⋃ ran A\} \in V$
11		fex2	$⊢ (({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}) : (B ∖ ran f) \times \{𝒫 ⋃ ran A\} ⟶ B ∖ ran f \land (B ∖ ran f) \times \{𝒫 ⋃ ran A\} \in V \land B ∖ ran f \in V) \to {1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})} \in V$
12	5 10 7 11	mp3an2i	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to {1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})} \in V$
13		unexg	$⊢ (f \in V \land {1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})} \in V) \to f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}) \in V$
14	4 12 13	sylancr	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}) \in V$
15		cnvexg	$⊢ f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}) \in V \to {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \in V$
16	14 15	syl	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \in V$
17		rnexg	$⊢ {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \in V \to ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \in V$
18	16 17	syl	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \in V$
19		simpl	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to f : A \underset{1-1}{⟶} B$
20		f1dm	$⊢ f : A \underset{1-1}{⟶} B \to dom f = A$
21	4	dmex	$⊢ dom f \in V$
22	20 21	eqeltrrdi	$⊢ f : A \underset{1-1}{⟶} B \to A \in V$
23	22	adantr	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to A \in V$
24		simpr	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to B \in V$
25		eqid	$⊢ {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} = {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
26	25	domss2	$⊢ (f : A \underset{1-1}{⟶} B \land A \in V \land B \in V) \to ({(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1 onto}{⟶} ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \land A \subseteq ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \land {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \circ f = {I ↾}_{A})$
27	19 23 24 26	syl3anc	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to ({(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1 onto}{⟶} ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \land A \subseteq ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \land {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \circ f = {I ↾}_{A})$
28	27	simp2d	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to A \subseteq ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
29	27	simp1d	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1 onto}{⟶} ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
30		f1oen3g	$⊢ ({(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \in V \land {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} : B \underset{1-1 onto}{⟶} ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1}) \to B \approx ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
31	16 29 30	syl2anc	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to B \approx ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1}$
32	28 31	jca	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to (A \subseteq ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \land B \approx ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1})$
33		sseq2	$⊢ x = ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \to (A \subseteq x \leftrightarrow A \subseteq ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1})$
34		breq2	$⊢ x = ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \to (B \approx x \leftrightarrow B \approx ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1})$
35	33 34	anbi12d	$⊢ x = ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \to ((A \subseteq x \land B \approx x) \leftrightarrow (A \subseteq ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1} \land B \approx ran {(f \cup ({1^{st} ↾}_{((B ∖ ran f) \times \{𝒫 ⋃ ran A\})}))}^{-1}))$
36	18 32 35	spcedv	$⊢ (f : A \underset{1-1}{⟶} B \land B \in V) \to \exists x (A \subseteq x \land B \approx x)$
37	36	ex	$⊢ f : A \underset{1-1}{⟶} B \to (B \in V \to \exists x (A \subseteq x \land B \approx x))$
38	37	exlimiv	$⊢ \exists f f : A \underset{1-1}{⟶} B \to (B \in V \to \exists x (A \subseteq x \land B \approx x))$
39	1 3 38	sylc	$⊢ A ≼ B \to \exists x (A \subseteq x \land B \approx x)$

Metamath Proof Explorer

Theorem domssex

Proof