Theorem r111

Description: The cumulative hierarchy is a one-to-one function. (Contributed by Mario Carneiro, 19-Apr-2013)

	Ref	Expression
Assertion	r111	⊢ 𝑅1 : On –1-1→ V

Proof

Step	Hyp	Ref	Expression
1		r1fnon	⊢ 𝑅1 Fn On
2		dffn2	⊢ ( 𝑅1 Fn On ↔ 𝑅1 : On ⟶ V )
3	1 2	mpbi	⊢ 𝑅1 : On ⟶ V
4		eloni	⊢ ( 𝑥 ∈ On → Ord 𝑥 )
5		eloni	⊢ ( 𝑦 ∈ On → Ord 𝑦 )
6		ordtri3or	⊢ ( ( Ord 𝑥 ∧ Ord 𝑦 ) → ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) )
7	4 5 6	syl2an	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) )
8		sdomirr	⊢ ¬ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑦 )
9		r1sdom	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → ( 𝑅1 ‘ 𝑥 ) ≺ ( 𝑅1 ‘ 𝑦 ) )
10		breq1	⊢ ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → ( ( 𝑅1 ‘ 𝑥 ) ≺ ( 𝑅1 ‘ 𝑦 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) )
11	9 10	syl5ibcom	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) )
12	8 11	mtoi	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → ¬ ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
13	12	3adant1	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → ¬ ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
14	13	pm2.21d	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
15	14	3expia	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 ∈ 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
16		ax-1	⊢ ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
17	16	a1i	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
18		r1sdom	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) )
19		breq2	⊢ ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → ( ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) )
20	18 19	syl5ibcom	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) )
21	8 20	mtoi	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
22	21	3adant2	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
23	22	pm2.21d	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
24	23	3expia	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ 𝑥 → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
25	15 17 24	3jaod	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
26	7 25	mpd	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
27	26	rgen2	⊢ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 )
28		dff13	⊢ ( 𝑅1 : On –1-1→ V ↔ ( 𝑅1 : On ⟶ V ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
29	3 27 28	mpbir2an	⊢ 𝑅1 : On –1-1→ V