| Step | Hyp | Ref
| Expression |
| 1 | | relsset 35889 |
. . 3
⊢ Rel SSet |
| 2 | 1 | brrelex1i 5741 |
. 2
⊢ (𝐴 SSet
𝐵 → 𝐴 ∈ V) |
| 3 | | brsset.1 |
. . 3
⊢ 𝐵 ∈ V |
| 4 | 3 | ssex 5321 |
. 2
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
| 5 | | breq1 5146 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 SSet 𝐵 ↔ 𝐴 SSet 𝐵)) |
| 6 | | sseq1 4009 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
| 7 | | opex 5469 |
. . . . . . 7
⊢
〈𝑥, 𝐵〉 ∈ V |
| 8 | 7 | elrn 5904 |
. . . . . 6
⊢
(〈𝑥, 𝐵〉 ∈ ran ( E ⊗
(V ∖ E )) ↔ ∃𝑦 𝑦( E ⊗ (V ∖ E ))〈𝑥, 𝐵〉) |
| 9 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 10 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 11 | 9, 10, 3 | brtxp 35881 |
. . . . . . . 8
⊢ (𝑦( E ⊗ (V ∖ E
))〈𝑥, 𝐵〉 ↔ (𝑦 E 𝑥 ∧ 𝑦(V ∖ E )𝐵)) |
| 12 | | epel 5587 |
. . . . . . . . 9
⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥) |
| 13 | | brv 5477 |
. . . . . . . . . . 11
⊢ 𝑦V𝐵 |
| 14 | | brdif 5196 |
. . . . . . . . . . 11
⊢ (𝑦(V ∖ E )𝐵 ↔ (𝑦V𝐵 ∧ ¬ 𝑦 E 𝐵)) |
| 15 | 13, 14 | mpbiran 709 |
. . . . . . . . . 10
⊢ (𝑦(V ∖ E )𝐵 ↔ ¬ 𝑦 E 𝐵) |
| 16 | 3 | epeli 5586 |
. . . . . . . . . 10
⊢ (𝑦 E 𝐵 ↔ 𝑦 ∈ 𝐵) |
| 17 | 15, 16 | xchbinx 334 |
. . . . . . . . 9
⊢ (𝑦(V ∖ E )𝐵 ↔ ¬ 𝑦 ∈ 𝐵) |
| 18 | 12, 17 | anbi12i 628 |
. . . . . . . 8
⊢ ((𝑦 E 𝑥 ∧ 𝑦(V ∖ E )𝐵) ↔ (𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝐵)) |
| 19 | 11, 18 | bitri 275 |
. . . . . . 7
⊢ (𝑦( E ⊗ (V ∖ E
))〈𝑥, 𝐵〉 ↔ (𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝐵)) |
| 20 | 19 | exbii 1848 |
. . . . . 6
⊢
(∃𝑦 𝑦( E ⊗ (V ∖ E
))〈𝑥, 𝐵〉 ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝐵)) |
| 21 | | exanali 1859 |
. . . . . 6
⊢
(∃𝑦(𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝐵) ↔ ¬ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) |
| 22 | 8, 20, 21 | 3bitrri 298 |
. . . . 5
⊢ (¬
∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵) ↔ 〈𝑥, 𝐵〉 ∈ ran ( E ⊗ (V ∖ E
))) |
| 23 | 22 | con1bii 356 |
. . . 4
⊢ (¬
〈𝑥, 𝐵〉 ∈ ran ( E ⊗ (V ∖ E
)) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) |
| 24 | | df-br 5144 |
. . . . 5
⊢ (𝑥 SSet
𝐵 ↔ 〈𝑥, 𝐵〉 ∈ SSet
) |
| 25 | | df-sset 35857 |
. . . . . . 7
⊢ SSet = ((V × V) ∖ ran ( E ⊗ (V
∖ E ))) |
| 26 | 25 | eleq2i 2833 |
. . . . . 6
⊢
(〈𝑥, 𝐵〉 ∈ SSet ↔ 〈𝑥, 𝐵〉 ∈ ((V × V) ∖ ran ( E
⊗ (V ∖ E )))) |
| 27 | 10, 3 | opelvv 5725 |
. . . . . . 7
⊢
〈𝑥, 𝐵〉 ∈ (V ×
V) |
| 28 | | eldif 3961 |
. . . . . . 7
⊢
(〈𝑥, 𝐵〉 ∈ ((V × V)
∖ ran ( E ⊗ (V ∖ E ))) ↔ (〈𝑥, 𝐵〉 ∈ (V × V) ∧ ¬
〈𝑥, 𝐵〉 ∈ ran ( E ⊗ (V ∖ E
)))) |
| 29 | 27, 28 | mpbiran 709 |
. . . . . 6
⊢
(〈𝑥, 𝐵〉 ∈ ((V × V)
∖ ran ( E ⊗ (V ∖ E ))) ↔ ¬ 〈𝑥, 𝐵〉 ∈ ran ( E ⊗ (V ∖ E
))) |
| 30 | 26, 29 | bitri 275 |
. . . . 5
⊢
(〈𝑥, 𝐵〉 ∈ SSet ↔ ¬ 〈𝑥, 𝐵〉 ∈ ran ( E ⊗ (V ∖ E
))) |
| 31 | 24, 30 | bitri 275 |
. . . 4
⊢ (𝑥 SSet
𝐵 ↔ ¬
〈𝑥, 𝐵〉 ∈ ran ( E ⊗ (V ∖ E
))) |
| 32 | | df-ss 3968 |
. . . 4
⊢ (𝑥 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) |
| 33 | 23, 31, 32 | 3bitr4i 303 |
. . 3
⊢ (𝑥 SSet
𝐵 ↔ 𝑥 ⊆ 𝐵) |
| 34 | 5, 6, 33 | vtoclbg 3557 |
. 2
⊢ (𝐴 ∈ V → (𝐴 SSet
𝐵 ↔ 𝐴 ⊆ 𝐵)) |
| 35 | 2, 4, 34 | pm5.21nii 378 |
1
⊢ (𝐴 SSet
𝐵 ↔ 𝐴 ⊆ 𝐵) |