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		ax1w	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
17		r1sdom	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) )
18		breq2	⊢ ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → ( ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) )
19	17 18	syl5ibcom	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑦 ) ) )
20	8 19	mtoi	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
21	20	3adant2	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
22	21	pm2.21d	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
23	22	3expia	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ 𝑥 → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
24	15 16 23	3jaod	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
25	7 24	mpd	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
26	25	rgen2	⊢ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 )
27		dff13	⊢ ( 𝑅1 : On –1-1→ V ↔ ( 𝑅1 : On ⟶ V ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
28	3 26 27	mpbir2an	⊢ 𝑅1 : On –1-1→ V