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

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)

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

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
2 1 alrimivv ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
3 df-rel ⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
4 df-ss ⊢ ( 𝐴 ⊆ ( V × V ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) )
5 3 4 sylbb ⊢ ( Rel 𝐴 → ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) )
6 elopabw ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) ) )
7 6 elv ⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) )
8 simpl ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
9 8 2eximi ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
10 7 9 sylbi ⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
11 df-xp ⊢ ( V × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
12 10 11 eleq2s ⊢ ( 𝑧 ∈ ( V × V ) → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
13 12 imim2i ⊢ ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) → ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
14 5 13 sylg ⊢ ( Rel 𝐴 → ∀ 𝑧 ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
15 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
16 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐵 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
17 15 16 imbi12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
18 17 biimprcd ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
19 18 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ∀ 𝑥 ∀ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
20 19.23vv ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
21 19 20 sylib ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
22 21 com23 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( 𝑧 ∈ 𝐴 → ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 ∈ 𝐵 ) ) )
23 22 a2d ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
24 23 alimdv ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
25 14 24 syl5 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( Rel 𝐴 → ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
26 df-ss ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) )
27 25 26 imbitrrdi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( Rel 𝐴 → 𝐴 ⊆ 𝐵 ) )
28 27 com12 ⊢ ( Rel 𝐴 → ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 ) )
29 2 28 impbid2 ⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )