This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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