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

Metamath Proof Explorer

Theorem ssrel2

Description: A subclass relationship depends only on a relation's ordered pairs. This version of ssrel is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018)

Ref Expression
Assertion ssrel2 ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑅 ⊆ 𝑆 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝑅 ⊆ 𝑆 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
2 1 a1d ⊢ ( 𝑅 ⊆ 𝑆 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) ) )
3 2 ralrimivv ⊢ ( 𝑅 ⊆ 𝑆 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
4 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
5 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑆 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
6 4 5 imbi12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) ) )
7 6 biimprcd ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) )
8 7 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) )
9 r19.23v ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) )
10 9 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) )
11 r19.23v ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) )
12 10 11 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) )
13 8 12 sylib ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) )
14 13 com23 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) → ( 𝑧 ∈ 𝑅 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 ∈ 𝑆 ) ) )
15 14 a2d ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) → ( ( 𝑧 ∈ 𝑅 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) )
16 15 alimdv ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑅 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ∀ 𝑧 ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) ) )
17 df-ss ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑅 → 𝑧 ∈ ( 𝐴 × 𝐵 ) ) )
18 elxp2 ⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
19 18 imbi2i ⊢ ( ( 𝑧 ∈ 𝑅 → 𝑧 ∈ ( 𝐴 × 𝐵 ) ) ↔ ( 𝑧 ∈ 𝑅 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
20 19 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑅 → 𝑧 ∈ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑅 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
21 17 20 bitri ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑅 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
22 df-ss ⊢ ( 𝑅 ⊆ 𝑆 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑆 ) )
23 16 21 22 3imtr4g ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) → ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → 𝑅 ⊆ 𝑆 ) )
24 23 com12 ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) → 𝑅 ⊆ 𝑆 ) )
25 3 24 impbid2 ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑅 ⊆ 𝑆 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) ) )