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 ⊢ 𝐵 ∈ V
Assertion brsset ( 𝐴 SSet 𝐵 ↔ 𝐴 ⊆ 𝐵 )

Proof

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