Step |
Hyp |
Ref |
Expression |
1 |
|
reltpos |
⊢ Rel tpos 𝐹 |
2 |
1
|
brrelex1i |
⊢ ( 𝐴 tpos 𝐹 𝐵 → 𝐴 ∈ V ) |
3 |
2
|
a1i |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 tpos 𝐹 𝐵 → 𝐴 ∈ V ) ) |
4 |
|
elex |
⊢ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) → 𝐴 ∈ V ) |
5 |
4
|
adantr |
⊢ ( ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) → 𝐴 ∈ V ) |
6 |
5
|
a1i |
⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) → 𝐴 ∈ V ) ) |
7 |
|
df-tpos |
⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) |
8 |
7
|
breqi |
⊢ ( 𝐴 tpos 𝐹 𝐵 ↔ 𝐴 ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) 𝐵 ) |
9 |
|
brcog |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) 𝐵 ↔ ∃ 𝑦 ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ) ) |
10 |
8 9
|
syl5bb |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 tpos 𝐹 𝐵 ↔ ∃ 𝑦 ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ) ) |
11 |
|
funmpt |
⊢ Fun ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) |
12 |
|
funbrfv2b |
⊢ ( Fun ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) → ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ↔ ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ∧ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ) ) ) |
13 |
11 12
|
ax-mp |
⊢ ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ↔ ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ∧ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ) ) |
14 |
|
snex |
⊢ { 𝑥 } ∈ V |
15 |
14
|
cnvex |
⊢ ◡ { 𝑥 } ∈ V |
16 |
15
|
uniex |
⊢ ∪ ◡ { 𝑥 } ∈ V |
17 |
|
eqid |
⊢ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) |
18 |
16 17
|
dmmpti |
⊢ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) = ( ◡ dom 𝐹 ∪ { ∅ } ) |
19 |
18
|
eleq2i |
⊢ ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ↔ 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) |
20 |
|
eqcom |
⊢ ( ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ↔ 𝑦 = ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) ) |
21 |
19 20
|
anbi12i |
⊢ ( ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ∧ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) ) ) |
22 |
|
sneq |
⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } ) |
23 |
22
|
cnveqd |
⊢ ( 𝑥 = 𝐴 → ◡ { 𝑥 } = ◡ { 𝐴 } ) |
24 |
23
|
unieqd |
⊢ ( 𝑥 = 𝐴 → ∪ ◡ { 𝑥 } = ∪ ◡ { 𝐴 } ) |
25 |
|
snex |
⊢ { 𝐴 } ∈ V |
26 |
25
|
cnvex |
⊢ ◡ { 𝐴 } ∈ V |
27 |
26
|
uniex |
⊢ ∪ ◡ { 𝐴 } ∈ V |
28 |
24 17 27
|
fvmpt |
⊢ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) → ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = ∪ ◡ { 𝐴 } ) |
29 |
28
|
eqeq2d |
⊢ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) → ( 𝑦 = ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) ↔ 𝑦 = ∪ ◡ { 𝐴 } ) ) |
30 |
29
|
pm5.32i |
⊢ ( ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ∪ ◡ { 𝐴 } ) ) |
31 |
21 30
|
bitri |
⊢ ( ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ∧ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ∪ ◡ { 𝐴 } ) ) |
32 |
13 31
|
bitri |
⊢ ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ∪ ◡ { 𝐴 } ) ) |
33 |
32
|
biancomi |
⊢ ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ↔ ( 𝑦 = ∪ ◡ { 𝐴 } ∧ 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) ) |
34 |
33
|
anbi1i |
⊢ ( ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ↔ ( ( 𝑦 = ∪ ◡ { 𝐴 } ∧ 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) ∧ 𝑦 𝐹 𝐵 ) ) |
35 |
|
anass |
⊢ ( ( ( 𝑦 = ∪ ◡ { 𝐴 } ∧ 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) ∧ 𝑦 𝐹 𝐵 ) ↔ ( 𝑦 = ∪ ◡ { 𝐴 } ∧ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ) ) |
36 |
34 35
|
bitri |
⊢ ( ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ↔ ( 𝑦 = ∪ ◡ { 𝐴 } ∧ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ) ) |
37 |
36
|
exbii |
⊢ ( ∃ 𝑦 ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 = ∪ ◡ { 𝐴 } ∧ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ) ) |
38 |
|
breq1 |
⊢ ( 𝑦 = ∪ ◡ { 𝐴 } → ( 𝑦 𝐹 𝐵 ↔ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) |
39 |
38
|
anbi2d |
⊢ ( 𝑦 = ∪ ◡ { 𝐴 } → ( ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) ) |
40 |
27 39
|
ceqsexv |
⊢ ( ∃ 𝑦 ( 𝑦 = ∪ ◡ { 𝐴 } ∧ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) |
41 |
37 40
|
bitri |
⊢ ( ∃ 𝑦 ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) |
42 |
10 41
|
bitrdi |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 tpos 𝐹 𝐵 ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) ) |
43 |
42
|
expcom |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ V → ( 𝐴 tpos 𝐹 𝐵 ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) ) ) |
44 |
3 6 43
|
pm5.21ndd |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 tpos 𝐹 𝐵 ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) ) |