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

Metamath Proof Explorer

Theorem ssrelrel

Description: A subclass relationship determined by ordered triples. Use relrelss to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion ssrelrel ( 𝐴 ⊆ ( ( V × V ) × V ) → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) )
2 1 alrimiv ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) )
3 2 alrimivv ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) )
4 elvvv ⊢ ( 𝑤 ∈ ( ( V × V ) × V ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
5 eleq1 ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ) )
6 eleq1 ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐵 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) )
7 5 6 imbi12d ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ) )
8 7 biimprcd ⊢ ( ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
9 8 alimi ⊢ ( ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ∀ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
10 19.23v ⊢ ( ∀ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) ↔ ( ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
11 9 10 sylib ⊢ ( ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ( ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
12 11 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
13 19.23vv ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
14 12 13 sylib ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
15 4 14 biimtrid ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ( 𝑤 ∈ ( ( V × V ) × V ) → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
16 15 com23 ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ( 𝑤 ∈ 𝐴 → ( 𝑤 ∈ ( ( V × V ) × V ) → 𝑤 ∈ 𝐵 ) ) )
17 16 a2d ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ( ( 𝑤 ∈ 𝐴 → 𝑤 ∈ ( ( V × V ) × V ) ) → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
18 17 alimdv ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝐴 → 𝑤 ∈ ( ( V × V ) × V ) ) → ∀ 𝑤 ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ) )
19 df-ss ⊢ ( 𝐴 ⊆ ( ( V × V ) × V ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝐴 → 𝑤 ∈ ( ( V × V ) × V ) ) )
20 df-ss ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) )
21 18 19 20 3imtr4g ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → ( 𝐴 ⊆ ( ( V × V ) × V ) → 𝐴 ⊆ 𝐵 ) )
22 21 com12 ⊢ ( 𝐴 ⊆ ( ( V × V ) × V ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 ) )
23 3 22 impbid2 ⊢ ( 𝐴 ⊆ ( ( V × V ) × V ) → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ) )