Step | Hyp | Ref
| Expression |
1 | | nfiu1 4550 |
. . . . . 6
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐴 𝐵 |
2 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑦𝐶 |
3 | 1, 2 | nfdisj 4632 |
. . . . 5
⊢
Ⅎ𝑦Disj
𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 |
4 | | ssiun2 4563 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → 𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
5 | | disjss1 4626 |
. . . . . . 7
⊢ (𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑥 ∈ 𝐵 𝐶)) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑥 ∈ 𝐵 𝐶)) |
7 | 6 | com12 32 |
. . . . 5
⊢
(Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → (𝑦 ∈ 𝐴 → Disj 𝑥 ∈ 𝐵 𝐶)) |
8 | 3, 7 | ralrimi 2957 |
. . . 4
⊢
(Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶) |
9 | 8 | a1i 11 |
. . 3
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶)) |
10 | | simplr 792 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) |
11 | | simprll 802 |
. . . . . . . . . . 11
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝐴) |
12 | | ssiun2 4563 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
13 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑢𝐵 |
14 | | nfcsb1v 3549 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦⦋𝑢 / 𝑦⦌𝐵 |
15 | | csbeq1a 3542 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑦⦌𝐵) |
16 | 13, 14, 15 | cbviun 4557 |
. . . . . . . . . . . 12
⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 |
17 | 12, 16 | syl6sseqr 3652 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
18 | 11, 17 | syl 17 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
19 | | simprlr 803 |
. . . . . . . . . . 11
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝐴) |
20 | | csbeq1 3536 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑣 → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
21 | 20 | sseq1d 3632 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵 ↔ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵)) |
22 | 21, 17 | vtoclga 3272 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
23 | 19, 22 | syl 17 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
24 | | simpl 473 |
. . . . . . . . . . . . . . . 16
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑦 ∈ 𝐴 𝐵) |
25 | 13, 14, 15 | cbvdisj 4630 |
. . . . . . . . . . . . . . . 16
⊢
(Disj 𝑦
∈ 𝐴 𝐵 ↔ Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
26 | 24, 25 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
27 | 20 | disjor 4634 |
. . . . . . . . . . . . . . 15
⊢
(Disj 𝑢
∈ 𝐴
⦋𝑢 / 𝑦⦌𝐵 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
28 | 26, 27 | sylib 208 |
. . . . . . . . . . . . . 14
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
29 | | rsp2 2936 |
. . . . . . . . . . . . . 14
⊢
(∀𝑢 ∈
𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))) |
31 | 30 | imp 445 |
. . . . . . . . . . . 12
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
32 | 31 | ord 392 |
. . . . . . . . . . 11
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
33 | 32 | impr 649 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) |
34 | | disjiun 4640 |
. . . . . . . . . 10
⊢
((Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ∧ (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵 ∧ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵 ∧ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
35 | 10, 18, 23, 33, 34 | syl13anc 1328 |
. . . . . . . . 9
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
36 | 35 | expr 643 |
. . . . . . . 8
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
37 | 36 | orrd 393 |
. . . . . . 7
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
38 | 37 | ralrimivva 2971 |
. . . . . 6
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
39 | 20 | iuneq1d 4545 |
. . . . . . 7
⊢ (𝑢 = 𝑣 → ∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) |
40 | 39 | disjor 4634 |
. . . . . 6
⊢
(Disj 𝑢
∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
41 | 38, 40 | sylibr 224 |
. . . . 5
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
42 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑢∪ 𝑥 ∈ 𝐵 𝐶 |
43 | 14, 2 | nfiun 4548 |
. . . . . 6
⊢
Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 |
44 | 15 | iuneq1d 4545 |
. . . . . 6
⊢ (𝑦 = 𝑢 → ∪
𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
45 | 42, 43, 44 | cbvdisj 4630 |
. . . . 5
⊢
(Disj 𝑦
∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
46 | 41, 45 | sylibr 224 |
. . . 4
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) |
47 | 46 | ex 450 |
. . 3
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) |
48 | 9, 47 | jcad 555 |
. 2
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))) |
49 | 16 | eleq2i 2693 |
. . . . . . . . 9
⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑟 ∈ ∪
𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
50 | | eliun 4524 |
. . . . . . . . 9
⊢ (𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
51 | 49, 50 | bitri 264 |
. . . . . . . 8
⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
52 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑣𝐵 |
53 | | nfcsb1v 3549 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐵 |
54 | | csbeq1a 3542 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑣 → 𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
55 | 52, 53, 54 | cbviun 4557 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵 |
56 | 55 | eleq2i 2693 |
. . . . . . . . 9
⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑠 ∈ ∪
𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵) |
57 | | eliun 4524 |
. . . . . . . . 9
⊢ (𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
58 | 56, 57 | bitri 264 |
. . . . . . . 8
⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
59 | 51, 58 | anbi12i 733 |
. . . . . . 7
⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
60 | | reeanv 3107 |
. . . . . . 7
⊢
(∃𝑢 ∈
𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
61 | 59, 60 | bitr4i 267 |
. . . . . 6
⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
62 | | simplrr 801 |
. . . . . . . . . . . 12
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ¬ 𝑟 = 𝑠) |
63 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → 𝑢 ∈ 𝐴) |
64 | | simplrl 800 |
. . . . . . . . . . . . . . . . 17
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶) |
65 | 14, 2 | nfdisj 4632 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦Disj
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 |
66 | 15 | disjeq1d 4628 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑢 → (Disj 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)) |
67 | 65, 66 | rspc 3303 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)) |
68 | 63, 64, 67 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
69 | 68 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
70 | | disjors 4635 |
. . . . . . . . . . . . . . 15
⊢
(Disj 𝑥
∈ ⦋ 𝑢 /
𝑦⦌𝐵𝐶 ↔ ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
71 | 69, 70 | sylib 208 |
. . . . . . . . . . . . . 14
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
72 | | simplrl 800 |
. . . . . . . . . . . . . . . 16
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
73 | 72 | simpld 475 |
. . . . . . . . . . . . . . 15
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
74 | 72 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
75 | 20 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
76 | 74, 75 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
77 | 73, 76 | jca 554 |
. . . . . . . . . . . . . 14
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)) |
78 | | rsp2 2936 |
. . . . . . . . . . . . . 14
⊢
(∀𝑟 ∈
⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
79 | 71, 77, 78 | sylc 65 |
. . . . . . . . . . . . 13
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
80 | 79 | ord 392 |
. . . . . . . . . . . 12
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
81 | 62, 80 | mpd 15 |
. . . . . . . . . . 11
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
82 | | simplrl 800 |
. . . . . . . . . . . . . . 15
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
83 | 82 | simpld 475 |
. . . . . . . . . . . . . 14
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
84 | | ssiun2 4563 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪
𝑟 ∈ ⦋
𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶) |
85 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑟𝐶 |
86 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑟 / 𝑥⦌𝐶 |
87 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑟 → 𝐶 = ⦋𝑟 / 𝑥⦌𝐶) |
88 | 85, 86, 87 | cbviun 4557 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶 |
89 | 84, 88 | syl6sseqr 3652 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶) |
90 | 83, 89 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶) |
91 | 82 | simprd 479 |
. . . . . . . . . . . . . 14
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
92 | | ssiun2 4563 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑠 ∈ ⦋
𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶) |
93 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑠𝐶 |
94 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐶 |
95 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑠 → 𝐶 = ⦋𝑠 / 𝑥⦌𝐶) |
96 | 93, 94, 95 | cbviun 4557 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶 = ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶 |
97 | 92, 96 | syl6sseqr 3652 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) |
98 | 91, 97 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) |
99 | | ss2in 3840 |
. . . . . . . . . . . . 13
⊢
((⦋𝑟 /
𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∧ ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶)) |
100 | 90, 98, 99 | syl2anc 693 |
. . . . . . . . . . . 12
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶)) |
101 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) |
102 | 101 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) |
103 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧∪ 𝑥 ∈ 𝐵 𝐶 |
104 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐵 |
105 | 104, 2 | nfiun 4548 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 |
106 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑦⦌𝐵) |
107 | 106 | iuneq1d 4545 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → ∪
𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
108 | 103, 105,
107 | cbvdisj 4630 |
. . . . . . . . . . . . . 14
⊢
(Disj 𝑦
∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
109 | 102, 108 | sylib 208 |
. . . . . . . . . . . . 13
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
110 | 63 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → 𝑢 ∈ 𝐴) |
111 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → 𝑣 ∈ 𝐴) |
112 | 111 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → 𝑣 ∈ 𝐴) |
113 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → 𝑢 ≠ 𝑣) |
114 | | csbeq1 3536 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑢 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑢 / 𝑦⦌𝐵) |
115 | 114 | iuneq1d 4545 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑢 → ∪
𝑥 ∈ ⦋
𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
116 | | csbeq1 3536 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑣 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
117 | 116 | iuneq1d 4545 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑣 → ∪
𝑥 ∈ ⦋
𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) |
118 | 115, 117 | disji2 4636 |
. . . . . . . . . . . . 13
⊢
((Disj 𝑧
∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣) → (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
119 | 109, 110,
112, 113, 118 | syl121anc 1331 |
. . . . . . . . . . . 12
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
120 | | sseq0 3975 |
. . . . . . . . . . . 12
⊢
(((⦋𝑟
/ 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) ∧ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
121 | 100, 119,
120 | syl2anc 693 |
. . . . . . . . . . 11
⊢
(((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
122 | 81, 121 | pm2.61dane 2881 |
. . . . . . . . . 10
⊢
((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
123 | 122 | expr 643 |
. . . . . . . . 9
⊢
((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
124 | 123 | orrd 393 |
. . . . . . . 8
⊢
((((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
125 | 124 | ex 450 |
. . . . . . 7
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
126 | 125 | rexlimdvva 3038 |
. . . . . 6
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
127 | 61, 126 | syl5bi 232 |
. . . . 5
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) → ((𝑟 ∈ ∪
𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
128 | 127 | ralrimivv 2970 |
. . . 4
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) → ∀𝑟 ∈ ∪
𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
129 | | disjors 4635 |
. . . 4
⊢
(Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ ∀𝑟 ∈ ∪
𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
130 | 128, 129 | sylibr 224 |
. . 3
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) → Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) |
131 | 130 | ex 450 |
. 2
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶)) |
132 | 48, 131 | impbid 202 |
1
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 ↔ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))) |