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

Metamath Proof Explorer

Theorem ssrelf

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) (Revised by Thierry Arnoux, 6-Nov-2017)

Ref Expression
Hypotheses eqrelrd2.1 ⊢ Ⅎ 𝑥 𝜑
eqrelrd2.2 ⊢ Ⅎ 𝑦 𝜑
eqrelrd2.3 ⊢ Ⅎ 𝑥 𝐴
eqrelrd2.4 ⊢ Ⅎ 𝑦 𝐴
eqrelrd2.5 ⊢ Ⅎ 𝑥 𝐵
eqrelrd2.6 ⊢ Ⅎ 𝑦 𝐵
Assertion ssrelf ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eqrelrd2.1 ⊢ Ⅎ 𝑥 𝜑
2 eqrelrd2.2 ⊢ Ⅎ 𝑦 𝜑
3 eqrelrd2.3 ⊢ Ⅎ 𝑥 𝐴
4 eqrelrd2.4 ⊢ Ⅎ 𝑦 𝐴
5 eqrelrd2.5 ⊢ Ⅎ 𝑥 𝐵
6 eqrelrd2.6 ⊢ Ⅎ 𝑦 𝐵
7 3 5 nfss ⊢ Ⅎ 𝑥 𝐴 ⊆ 𝐵
8 4 6 nfss ⊢ Ⅎ 𝑦 𝐴 ⊆ 𝐵
9 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
10 8 9 alrimi ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
11 7 10 alrimi ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
12 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
13 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐵 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
14 12 13 imbi12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
15 14 biimprcd ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
16 15 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ∀ 𝑥 ∀ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
17 4 nfcri ⊢ Ⅎ 𝑦 𝑧 ∈ 𝐴
18 6 nfcri ⊢ Ⅎ 𝑦 𝑧 ∈ 𝐵
19 17 18 nfim ⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 )
20 19 19.23 ⊢ ( ∀ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) ↔ ( ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
21 20 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) ↔ ∀ 𝑥 ( ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
22 3 nfcri ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
23 5 nfcri ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐵
24 22 23 nfim ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 )
25 24 19.23 ⊢ ( ∀ 𝑥 ( ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
26 21 25 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
27 16 26 sylib ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
28 27 com23 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( 𝑧 ∈ 𝐴 → ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 ∈ 𝐵 ) ) )
29 28 a2d ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
30 29 alimdv ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
31 df-rel ⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
32 df-ss ⊢ ( 𝐴 ⊆ ( V × V ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) )
33 elvv ⊢ ( 𝑧 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
34 33 imbi2i ⊢ ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) ↔ ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
35 34 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
36 31 32 35 3bitri ⊢ ( Rel 𝐴 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
37 df-ss ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) )
38 30 36 37 3imtr4g ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( Rel 𝐴 → 𝐴 ⊆ 𝐵 ) )
39 38 com12 ⊢ ( Rel 𝐴 → ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 ) )
40 11 39 impbid2 ⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )