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 | r1ord3 | ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r1fnon | ⊢ 𝑅1 Fn On | |
2 | 1 | fndmi | ⊢ dom 𝑅1 = On |
3 | 2 | eleq2i | ⊢ ( 𝐴 ∈ dom 𝑅1 ↔ 𝐴 ∈ On ) |
4 | 2 | eleq2i | ⊢ ( 𝐵 ∈ dom 𝑅1 ↔ 𝐵 ∈ On ) |
5 | r1ord3g | ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) ) | |
6 | 3 4 5 | syl2anbr | ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) ) |