oacomf1olem

		Ref	Expression
	Hypothesis	oacomf1olem.1	$⊢ F = (x \in A ⟼ B +_{𝑜} x)$
	Assertion	oacomf1olem	$⊢ (A \in On \land B \in On) \to (F : A \underset{1-1 onto}{⟶} ran F \land ran F \cap B = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		oacomf1olem.1	$⊢ F = (x \in A ⟼ B +_{𝑜} x)$
2		oaf1o	$⊢ B \in On \to (x \in On ⟼ B +_{𝑜} x) : On \underset{1-1 onto}{⟶} On ∖ B$
3	2	adantl	$⊢ (A \in On \land B \in On) \to (x \in On ⟼ B +_{𝑜} x) : On \underset{1-1 onto}{⟶} On ∖ B$
4		f1of1	$⊢ (x \in On ⟼ B +_{𝑜} x) : On \underset{1-1 onto}{⟶} On ∖ B \to (x \in On ⟼ B +_{𝑜} x) : On \underset{1-1}{⟶} On ∖ B$
5	3 4	syl	$⊢ (A \in On \land B \in On) \to (x \in On ⟼ B +_{𝑜} x) : On \underset{1-1}{⟶} On ∖ B$
6		onss	$⊢ A \in On \to A \subseteq On$
7	6	adantr	$⊢ (A \in On \land B \in On) \to A \subseteq On$
8		f1ssres	$⊢ ((x \in On ⟼ B +_{𝑜} x) : On \underset{1-1}{⟶} On ∖ B \land A \subseteq On) \to ({(x \in On ⟼ B +_{𝑜} x) ↾}_{A}) : A \underset{1-1}{⟶} On ∖ B$
9	5 7 8	syl2anc	$⊢ (A \in On \land B \in On) \to ({(x \in On ⟼ B +_{𝑜} x) ↾}_{A}) : A \underset{1-1}{⟶} On ∖ B$
10	7	resmptd	$⊢ (A \in On \land B \in On) \to {(x \in On ⟼ B +_{𝑜} x) ↾}_{A} = (x \in A ⟼ B +_{𝑜} x)$
11	10 1	eqtr4di	$⊢ (A \in On \land B \in On) \to {(x \in On ⟼ B +_{𝑜} x) ↾}_{A} = F$
12		f1eq1	$⊢ {(x \in On ⟼ B +_{𝑜} x) ↾}_{A} = F \to (({(x \in On ⟼ B +_{𝑜} x) ↾}_{A}) : A \underset{1-1}{⟶} On ∖ B \leftrightarrow F : A \underset{1-1}{⟶} On ∖ B)$
13	11 12	syl	$⊢ (A \in On \land B \in On) \to (({(x \in On ⟼ B +_{𝑜} x) ↾}_{A}) : A \underset{1-1}{⟶} On ∖ B \leftrightarrow F : A \underset{1-1}{⟶} On ∖ B)$
14	9 13	mpbid	$⊢ (A \in On \land B \in On) \to F : A \underset{1-1}{⟶} On ∖ B$
15		f1f1orn	$⊢ F : A \underset{1-1}{⟶} On ∖ B \to F : A \underset{1-1 onto}{⟶} ran F$
16	14 15	syl	$⊢ (A \in On \land B \in On) \to F : A \underset{1-1 onto}{⟶} ran F$
17		f1f	$⊢ F : A \underset{1-1}{⟶} On ∖ B \to F : A ⟶ On ∖ B$
18		frn	$⊢ F : A ⟶ On ∖ B \to ran F \subseteq On ∖ B$
19	14 17 18	3syl	$⊢ (A \in On \land B \in On) \to ran F \subseteq On ∖ B$
20	19	difss2d	$⊢ (A \in On \land B \in On) \to ran F \subseteq On$
21		reldisj	$⊢ ran F \subseteq On \to (ran F \cap B = \emptyset \leftrightarrow ran F \subseteq On ∖ B)$
22	20 21	syl	$⊢ (A \in On \land B \in On) \to (ran F \cap B = \emptyset \leftrightarrow ran F \subseteq On ∖ B)$
23	19 22	mpbird	$⊢ (A \in On \land B \in On) \to ran F \cap B = \emptyset$
24	16 23	jca	$⊢ (A \in On \land B \in On) \to (F : A \underset{1-1 onto}{⟶} ran F \land ran F \cap B = \emptyset)$

Metamath Proof Explorer

Theorem oacomf1olem

Proof