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

Metamath Proof Explorer

Theorem r1ord3g

Description: Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of BellMachover p. 478. (Contributed by NM, 22-Sep-2003)

Ref Expression
Assertion r1ord3g ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
2 1 simpri ⊢ Lim dom 𝑅1
3 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
4 ordsson ⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
5 2 3 4 mp2b ⊢ dom 𝑅1 ⊆ On
6 5 sseli ⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ∈ On )
7 5 sseli ⊢ ( 𝐵 ∈ dom 𝑅1 → 𝐵 ∈ On )
8 onsseleq ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
9 6 7 8 syl2an ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
10 r1tr ⊢ Tr ( 𝑅1 ‘ 𝐵 )
11 r1ordg ⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) )
12 11 adantl ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) )
13 trss ⊢ ( Tr ( 𝑅1 ‘ 𝐵 ) → ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
14 10 12 13 mpsylsyld ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
15 fveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑅1 ‘ 𝐴 ) = ( 𝑅1 ‘ 𝐵 ) )
16 eqimss ⊢ ( ( 𝑅1 ‘ 𝐴 ) = ( 𝑅1 ‘ 𝐵 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) )
17 15 16 syl ⊢ ( 𝐴 = 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) )
18 17 a1i ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 = 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
19 14 18 jaod ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
20 9 19 sylbid ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )