r111

Description: The cumulative hierarchy of sets is a one-to-one function. Use r1fun or r1fnon (which require fewer axioms) when sufficient. (Contributed by Mario Carneiro, 19-Apr-2013)

		Ref	Expression
	Assertion	r111	$⊢ R_{1} : On \underset{1-1}{⟶} V$

Proof

Step	Hyp	Ref	Expression
1		r1fnon	$⊢ R_{1} Fn On$
2		dffn2	$⊢ R_{1} Fn On \leftrightarrow R_{1} : On ⟶ V$
3	1 2	mpbi	$⊢ R_{1} : On ⟶ V$
4		eloni	$⊢ x \in On \to Ord x$
5		eloni	$⊢ y \in On \to Ord y$
6		ordtri3or	$⊢ (Ord x \land Ord y) \to (x \in y \lor x = y \lor y \in x)$
7	4 5 6	syl2an	$⊢ (x \in On \land y \in On) \to (x \in y \lor x = y \lor y \in x)$
8		sdomirr	$⊢ \neg R_{1} (y) ≺ R_{1} (y)$
9		r1sdom	$⊢ (y \in On \land x \in y) \to R_{1} (x) ≺ R_{1} (y)$
10		breq1	$⊢ R_{1} (x) = R_{1} (y) \to (R_{1} (x) ≺ R_{1} (y) \leftrightarrow R_{1} (y) ≺ R_{1} (y))$
11	9 10	syl5ibcom	$⊢ (y \in On \land x \in y) \to (R_{1} (x) = R_{1} (y) \to R_{1} (y) ≺ R_{1} (y))$
12	8 11	mtoi	$⊢ (y \in On \land x \in y) \to \neg R_{1} (x) = R_{1} (y)$
13	12	3adant1	$⊢ (x \in On \land y \in On \land x \in y) \to \neg R_{1} (x) = R_{1} (y)$
14	13	pm2.21d	$⊢ (x \in On \land y \in On \land x \in y) \to (R_{1} (x) = R_{1} (y) \to x = y)$
15	14	3expia	$⊢ (x \in On \land y \in On) \to (x \in y \to (R_{1} (x) = R_{1} (y) \to x = y))$
16		ax1w	$⊢ (x \in On \land y \in On) \to (x = y \to (R_{1} (x) = R_{1} (y) \to x = y))$
17		r1sdom	$⊢ (x \in On \land y \in x) \to R_{1} (y) ≺ R_{1} (x)$
18		breq2	$⊢ R_{1} (x) = R_{1} (y) \to (R_{1} (y) ≺ R_{1} (x) \leftrightarrow R_{1} (y) ≺ R_{1} (y))$
19	17 18	syl5ibcom	$⊢ (x \in On \land y \in x) \to (R_{1} (x) = R_{1} (y) \to R_{1} (y) ≺ R_{1} (y))$
20	8 19	mtoi	$⊢ (x \in On \land y \in x) \to \neg R_{1} (x) = R_{1} (y)$
21	20	3adant2	$⊢ (x \in On \land y \in On \land y \in x) \to \neg R_{1} (x) = R_{1} (y)$
22	21	pm2.21d	$⊢ (x \in On \land y \in On \land y \in x) \to (R_{1} (x) = R_{1} (y) \to x = y)$
23	22	3expia	$⊢ (x \in On \land y \in On) \to (y \in x \to (R_{1} (x) = R_{1} (y) \to x = y))$
24	15 16 23	3jaod	$⊢ (x \in On \land y \in On) \to ((x \in y \lor x = y \lor y \in x) \to (R_{1} (x) = R_{1} (y) \to x = y))$
25	7 24	mpd	$⊢ (x \in On \land y \in On) \to (R_{1} (x) = R_{1} (y) \to x = y)$
26	25	rgen2	$⊢ \forall x \in On \forall y \in On (R_{1} (x) = R_{1} (y) \to x = y)$
27		dff13	$⊢ R_{1} : On \underset{1-1}{⟶} V \leftrightarrow (R_{1} : On ⟶ V \land \forall x \in On \forall y \in On (R_{1} (x) = R_{1} (y) \to x = y))$
28	3 26 27	mpbir2an	$⊢ R_{1} : On \underset{1-1}{⟶} V$

Metamath Proof Explorer

Theorem r111

Proof