Metamath Proof Explorer

Theorem ssrel

Description: A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of Monk1 p. 33. (Contributed by NM, 2-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) Remove dependency on ax-12 . (Revised by SN, 11-Dec-2024) (Proof shortened by BJ, 5-Nov-2026)

Ref Expression
Assertion ssrel ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
2 1 alrimivv ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
3 df-rel ⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
4 ssel ⊢ ( 𝐴 ⊆ ( V × V ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) )
5 3 4 sylbi ⊢ ( Rel 𝐴 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) )
6 elxpi ⊢ ( 𝑧 ∈ ( V × V ) → ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) )
7 5 6 syl6 ⊢ ( Rel 𝐴 → ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) ) )
8 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
9 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐵 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
10 8 9 imbi12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
11 10 adantr ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
12 11 biimprcd ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
13 12 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
14 19.23vv ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
15 13 14 sylib ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
16 7 15 sylan9 ⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
17 16 pm2.43d ⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) )
18 17 ssrdv ⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) → 𝐴 ⊆ 𝐵 )
19 18 ex ⊢ ( Rel 𝐴 → ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 ) )
20 2 19 impbid2 ⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )