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 ‘ 𝐵 ) ) )