r111

Description: The cumulative hierarchy is a one-to-one function. (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		ax-1	$⊢ x = y \to (R_{1} (x) = R_{1} (y) \to x = y)$
17	16	a1i	$⊢ (x \in On \land y \in On) \to (x = y \to (R_{1} (x) = R_{1} (y) \to x = y))$
18		r1sdom	$⊢ (x \in On \land y \in x) \to R_{1} (y) ≺ R_{1} (x)$
19		breq2	$⊢ R_{1} (x) = R_{1} (y) \to (R_{1} (y) ≺ R_{1} (x) \leftrightarrow R_{1} (y) ≺ R_{1} (y))$
20	18 19	syl5ibcom	$⊢ (x \in On \land y \in x) \to (R_{1} (x) = R_{1} (y) \to R_{1} (y) ≺ R_{1} (y))$
21	8 20	mtoi	$⊢ (x \in On \land y \in x) \to \neg R_{1} (x) = R_{1} (y)$
22	21	3adant2	$⊢ (x \in On \land y \in On \land y \in x) \to \neg R_{1} (x) = R_{1} (y)$
23	22	pm2.21d	$⊢ (x \in On \land y \in On \land y \in x) \to (R_{1} (x) = R_{1} (y) \to x = y)$
24	23	3expia	$⊢ (x \in On \land y \in On) \to (y \in x \to (R_{1} (x) = R_{1} (y) \to x = y))$
25	15 17 24	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))$
26	7 25	mpd	$⊢ (x \in On \land y \in On) \to (R_{1} (x) = R_{1} (y) \to x = y)$
27	26	rgen2	$⊢ \forall x \in On \forall y \in On (R_{1} (x) = R_{1} (y) \to x = y)$
28		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))$
29	3 27 28	mpbir2an	$⊢ R_{1} : On \underset{1-1}{⟶} V$

Metamath Proof Explorer

Theorem r111

Proof