| Step | Hyp | Ref
| Expression |
| 1 | | reltpos 8256 |
. . . 4
⊢ Rel tpos
𝐹 |
| 2 | 1 | brrelex1i 5741 |
. . 3
⊢ (𝐴tpos 𝐹𝐵 → 𝐴 ∈ V) |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝐵 ∈ 𝑉 → (𝐴tpos 𝐹𝐵 → 𝐴 ∈ V)) |
| 4 | | elex 3501 |
. . . 4
⊢ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) → 𝐴 ∈ V) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵) → 𝐴 ∈ V) |
| 6 | 5 | a1i 11 |
. 2
⊢ (𝐵 ∈ 𝑉 → ((𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵) → 𝐴 ∈ V)) |
| 7 | | df-tpos 8251 |
. . . . . 6
⊢ tpos
𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) |
| 8 | 7 | breqi 5149 |
. . . . 5
⊢ (𝐴tpos 𝐹𝐵 ↔ 𝐴(𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))𝐵) |
| 9 | | brcog 5877 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝐴(𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))𝐵 ↔ ∃𝑦(𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ∧ 𝑦𝐹𝐵))) |
| 10 | 8, 9 | bitrid 283 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝐴tpos 𝐹𝐵 ↔ ∃𝑦(𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ∧ 𝑦𝐹𝐵))) |
| 11 | | funmpt 6604 |
. . . . . . . . . . 11
⊢ Fun
(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) |
| 12 | | funbrfv2b 6966 |
. . . . . . . . . . 11
⊢ (Fun
(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) → (𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ↔ (𝐴 ∈ dom (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ∧ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴) = 𝑦))) |
| 13 | 11, 12 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ↔ (𝐴 ∈ dom (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ∧ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴) = 𝑦)) |
| 14 | | snex 5436 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥} ∈ V |
| 15 | 14 | cnvex 7947 |
. . . . . . . . . . . . . . 15
⊢ ◡{𝑥} ∈ V |
| 16 | 15 | uniex 7761 |
. . . . . . . . . . . . . 14
⊢ ∪ ◡{𝑥} ∈ V |
| 17 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) |
| 18 | 16, 17 | dmmpti 6712 |
. . . . . . . . . . . . 13
⊢ dom
(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) = (◡dom 𝐹 ∪ {∅}) |
| 19 | 18 | eleq2i 2833 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ↔ 𝐴 ∈ (◡dom 𝐹 ∪ {∅})) |
| 20 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴) = 𝑦 ↔ 𝑦 = ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴)) |
| 21 | 19, 20 | anbi12i 628 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ∧ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴) = 𝑦) ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦 = ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴))) |
| 22 | | sneq 4636 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴}) |
| 23 | 22 | cnveqd 5886 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → ◡{𝑥} = ◡{𝐴}) |
| 24 | 23 | unieqd 4920 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → ∪ ◡{𝑥} = ∪ ◡{𝐴}) |
| 25 | | snex 5436 |
. . . . . . . . . . . . . . . 16
⊢ {𝐴} ∈ V |
| 26 | 25 | cnvex 7947 |
. . . . . . . . . . . . . . 15
⊢ ◡{𝐴} ∈ V |
| 27 | 26 | uniex 7761 |
. . . . . . . . . . . . . 14
⊢ ∪ ◡{𝐴} ∈ V |
| 28 | 24, 17, 27 | fvmpt 7016 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) → ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴) = ∪ ◡{𝐴}) |
| 29 | 28 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) → (𝑦 = ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴) ↔ 𝑦 = ∪ ◡{𝐴})) |
| 30 | 29 | pm5.32i 574 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦 = ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴)) ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦 = ∪ ◡{𝐴})) |
| 31 | 21, 30 | bitri 275 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ∧ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})‘𝐴) = 𝑦) ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦 = ∪ ◡{𝐴})) |
| 32 | 13, 31 | bitri 275 |
. . . . . . . . 9
⊢ (𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦 = ∪ ◡{𝐴})) |
| 33 | 32 | biancomi 462 |
. . . . . . . 8
⊢ (𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ↔ (𝑦 = ∪ ◡{𝐴} ∧ 𝐴 ∈ (◡dom 𝐹 ∪ {∅}))) |
| 34 | 33 | anbi1i 624 |
. . . . . . 7
⊢ ((𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ∧ 𝑦𝐹𝐵) ↔ ((𝑦 = ∪ ◡{𝐴} ∧ 𝐴 ∈ (◡dom 𝐹 ∪ {∅})) ∧ 𝑦𝐹𝐵)) |
| 35 | | anass 468 |
. . . . . . 7
⊢ (((𝑦 = ∪
◡{𝐴} ∧ 𝐴 ∈ (◡dom 𝐹 ∪ {∅})) ∧ 𝑦𝐹𝐵) ↔ (𝑦 = ∪ ◡{𝐴} ∧ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦𝐹𝐵))) |
| 36 | 34, 35 | bitri 275 |
. . . . . 6
⊢ ((𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ∧ 𝑦𝐹𝐵) ↔ (𝑦 = ∪ ◡{𝐴} ∧ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦𝐹𝐵))) |
| 37 | 36 | exbii 1848 |
. . . . 5
⊢
(∃𝑦(𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ∧ 𝑦𝐹𝐵) ↔ ∃𝑦(𝑦 = ∪ ◡{𝐴} ∧ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦𝐹𝐵))) |
| 38 | | breq1 5146 |
. . . . . . 7
⊢ (𝑦 = ∪
◡{𝐴} → (𝑦𝐹𝐵 ↔ ∪ ◡{𝐴}𝐹𝐵)) |
| 39 | 38 | anbi2d 630 |
. . . . . 6
⊢ (𝑦 = ∪
◡{𝐴} → ((𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦𝐹𝐵) ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵))) |
| 40 | 27, 39 | ceqsexv 3532 |
. . . . 5
⊢
(∃𝑦(𝑦 = ∪
◡{𝐴} ∧ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 𝑦𝐹𝐵)) ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵)) |
| 41 | 37, 40 | bitri 275 |
. . . 4
⊢
(∃𝑦(𝐴(𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})𝑦 ∧ 𝑦𝐹𝐵) ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵)) |
| 42 | 10, 41 | bitrdi 287 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵))) |
| 43 | 42 | expcom 413 |
. 2
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ V → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵)))) |
| 44 | 3, 6, 43 | pm5.21ndd 379 |
1
⊢ (𝐵 ∈ 𝑉 → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵))) |