Metamath Proof Explorer

Theorem brsset

Description: For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Hypothesis brsset.1 ⊢ B ∈ V
Assertion brsset ⊢ A 𝖲𝖲𝖾𝗍 B ↔ A ⊆ B

Proof

Step Hyp Ref Expression
1 brsset.1 ⊢ B ∈ V
2 relsset ⊢ Rel ⁡ 𝖲𝖲𝖾𝗍
3 2 brrelex1i ⊢ A 𝖲𝖲𝖾𝗍 B → A ∈ V
4 1 ssex ⊢ A ⊆ B → A ∈ V
5 breq1 ⊢ x = A → x 𝖲𝖲𝖾𝗍 B ↔ A 𝖲𝖲𝖾𝗍 B
6 sseq1 ⊢ x = A → x ⊆ B ↔ A ⊆ B
7 opex ⊢ x B ∈ V
8 7 elrn ⊢ x B ∈ ran ⁡ E ⊗ V ∖ E ↔ ∃ y y E ⊗ V ∖ E x B
9 vex ⊢ y ∈ V
10 vex ⊢ x ∈ V
11 9 10 1 brtxp ⊢ y E ⊗ V ∖ E x B ↔ y E x ∧ y V ∖ E B
12 epel ⊢ y E x ↔ y ∈ x
13 brv ⊢ y V B
14 brdif ⊢ y V ∖ E B ↔ y V B ∧ ¬ y E B
15 13 14 mpbiran ⊢ y V ∖ E B ↔ ¬ y E B
16 1 epeli ⊢ y E B ↔ y ∈ B
17 15 16 xchbinx ⊢ y V ∖ E B ↔ ¬ y ∈ B
18 12 17 anbi12i ⊢ y E x ∧ y V ∖ E B ↔ y ∈ x ∧ ¬ y ∈ B
19 11 18 bitri ⊢ y E ⊗ V ∖ E x B ↔ y ∈ x ∧ ¬ y ∈ B
20 19 exbii ⊢ ∃ y y E ⊗ V ∖ E x B ↔ ∃ y y ∈ x ∧ ¬ y ∈ B
21 exanali ⊢ ∃ y y ∈ x ∧ ¬ y ∈ B ↔ ¬ ∀ y y ∈ x → y ∈ B
22 8 20 21 3bitrri ⊢ ¬ ∀ y y ∈ x → y ∈ B ↔ x B ∈ ran ⁡ E ⊗ V ∖ E
23 22 con1bii ⊢ ¬ x B ∈ ran ⁡ E ⊗ V ∖ E ↔ ∀ y y ∈ x → y ∈ B
24 df-br ⊢ x 𝖲𝖲𝖾𝗍 B ↔ x B ∈ 𝖲𝖲𝖾𝗍
25 df-sset ⊢ 𝖲𝖲𝖾𝗍 = V × V ∖ ran ⁡ E ⊗ V ∖ E
26 25 eleq2i ⊢ x B ∈ 𝖲𝖲𝖾𝗍 ↔ x B ∈ V × V ∖ ran ⁡ E ⊗ V ∖ E
27 10 1 opelvv ⊢ x B ∈ V × V
28 eldif ⊢ x B ∈ V × V ∖ ran ⁡ E ⊗ V ∖ E ↔ x B ∈ V × V ∧ ¬ x B ∈ ran ⁡ E ⊗ V ∖ E
29 27 28 mpbiran ⊢ x B ∈ V × V ∖ ran ⁡ E ⊗ V ∖ E ↔ ¬ x B ∈ ran ⁡ E ⊗ V ∖ E
30 26 29 bitri ⊢ x B ∈ 𝖲𝖲𝖾𝗍 ↔ ¬ x B ∈ ran ⁡ E ⊗ V ∖ E
31 24 30 bitri ⊢ x 𝖲𝖲𝖾𝗍 B ↔ ¬ x B ∈ ran ⁡ E ⊗ V ∖ E
32 df-ss ⊢ x ⊆ B ↔ ∀ y y ∈ x → y ∈ B
33 23 31 32 3bitr4i ⊢ x 𝖲𝖲𝖾𝗍 B ↔ x ⊆ B
34 5 6 33 vtoclbg ⊢ A ∈ V → A 𝖲𝖲𝖾𝗍 B ↔ A ⊆ B
35 3 4 34 pm5.21nii ⊢ A 𝖲𝖲𝖾𝗍 B ↔ A ⊆ B