Step | Hyp | Ref
| Expression |
1 | | nfdisj1 4867 |
. . . 4
⊢
Ⅎ𝑥Disj
𝑥 ∈ 𝐴 𝐵 |
2 | | nfcv 2934 |
. . . . 5
⊢
Ⅎ𝑥𝑦 |
3 | | nfv 1957 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑖 ∈ 𝐴 |
4 | | nfcsb1v 3767 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵 |
5 | 4 | nfcri 2929 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵 |
6 | 3, 5 | nfan 1946 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) |
7 | 6 | nfab 2940 |
. . . . . . . 8
⊢
Ⅎ𝑥{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} |
8 | 7 | nfuni 4677 |
. . . . . . 7
⊢
Ⅎ𝑥∪ {𝑖
∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} |
9 | 8 | nfcsb1 3766 |
. . . . . 6
⊢
Ⅎ𝑥⦋∪
{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 |
10 | 9 | nfeq1 2947 |
. . . . 5
⊢
Ⅎ𝑥⦋∪
{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 |
11 | 2, 10 | nfral 3127 |
. . . 4
⊢
Ⅎ𝑥∀𝑗 ∈ 𝑦 ⦋∪
{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 |
12 | | eqeq2 2789 |
. . . . 5
⊢ (𝑦 = 𝐵 → (⦋∪ {𝑖
∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ⦋∪ {𝑖
∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)) |
13 | 12 | raleqbi1dv 3328 |
. . . 4
⊢ (𝑦 = 𝐵 → (∀𝑗 ∈ 𝑦 ⦋∪
{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ∀𝑗 ∈ 𝐵 ⦋∪
{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)) |
14 | | vex 3401 |
. . . . 5
⊢ 𝑦 ∈ V |
15 | 14 | a1i 11 |
. . . 4
⊢
(Disj 𝑥
∈ 𝐴 𝐵 → 𝑦 ∈ V) |
16 | | simplll 765 |
. . . . . . . . . . . . 13
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → Disj 𝑥 ∈ 𝐴 𝐵) |
17 | | simpllr 766 |
. . . . . . . . . . . . 13
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 ∈ 𝐴) |
18 | | simprl 761 |
. . . . . . . . . . . . 13
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑖 ∈ 𝐴) |
19 | | simplr 759 |
. . . . . . . . . . . . 13
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑗 ∈ 𝐵) |
20 | | simprr 763 |
. . . . . . . . . . . . 13
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) |
21 | | csbeq1a 3760 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵) |
22 | 4, 21 | disjif 29954 |
. . . . . . . . . . . . 13
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ 𝐵 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖) |
23 | 16, 17, 18, 19, 20, 22 | syl122anc 1447 |
. . . . . . . . . . . 12
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖) |
24 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖) |
25 | | simpllr 766 |
. . . . . . . . . . . . . 14
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 ∈ 𝐴) |
26 | 24, 25 | eqeltrrd 2860 |
. . . . . . . . . . . . 13
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑖 ∈ 𝐴) |
27 | | simplr 759 |
. . . . . . . . . . . . . 14
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑗 ∈ 𝐵) |
28 | 21 | eleq2d 2845 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑖 → (𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) |
29 | 24, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → (𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) |
30 | 27, 29 | mpbid 224 |
. . . . . . . . . . . . 13
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) |
31 | 26, 30 | jca 507 |
. . . . . . . . . . . 12
⊢
((((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) |
32 | 23, 31 | impbida 791 |
. . . . . . . . . . 11
⊢
(((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) ↔ 𝑥 = 𝑖)) |
33 | | equcom 2065 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑖 ↔ 𝑖 = 𝑥) |
34 | 32, 33 | syl6bb 279 |
. . . . . . . . . 10
⊢
(((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) ↔ 𝑖 = 𝑥)) |
35 | 34 | abbidv 2906 |
. . . . . . . . 9
⊢
(((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑖 ∣ 𝑖 = 𝑥}) |
36 | | df-sn 4399 |
. . . . . . . . 9
⊢ {𝑥} = {𝑖 ∣ 𝑖 = 𝑥} |
37 | 35, 36 | syl6eqr 2832 |
. . . . . . . 8
⊢
(((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑥}) |
38 | 37 | unieqd 4681 |
. . . . . . 7
⊢
(((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = ∪ {𝑥}) |
39 | | vex 3401 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
40 | 39 | unisn 4687 |
. . . . . . 7
⊢ ∪ {𝑥}
= 𝑥 |
41 | 38, 40 | syl6eq 2830 |
. . . . . 6
⊢
(((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥) |
42 | | csbeq1 3754 |
. . . . . . 7
⊢ (∪ {𝑖
∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖
∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = ⦋𝑥 / 𝑥⦌𝐵) |
43 | | csbid 3759 |
. . . . . . 7
⊢
⦋𝑥 /
𝑥⦌𝐵 = 𝐵 |
44 | 42, 43 | syl6eq 2830 |
. . . . . 6
⊢ (∪ {𝑖
∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖
∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵) |
45 | 41, 44 | syl 17 |
. . . . 5
⊢
(((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ⦋∪ {𝑖
∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵) |
46 | 45 | ralrimiva 3148 |
. . . 4
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → ∀𝑗 ∈ 𝐵 ⦋∪
{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵) |
47 | 1, 11, 13, 15, 46 | elabreximd 29910 |
. . 3
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ∀𝑗 ∈ 𝑦 ⦋∪
{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦) |
48 | 47 | ralrimiva 3148 |
. 2
⊢
(Disj 𝑥
∈ 𝐴 𝐵 → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪
{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦) |
49 | | invdisj 4872 |
. 2
⊢
(∀𝑦 ∈
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪
{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦) |
50 | 48, 49 | syl 17 |
1
⊢
(Disj 𝑥
∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦) |