Step | Hyp | Ref
| Expression |
1 | | nfiu1 4486 |
. . . . . 6
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐴 𝐵 |
2 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑦𝐶 |
3 | 1, 2 | nfdisj 4565 |
. . . . 5
⊢
Ⅎ𝑦Disj
𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 |
4 | | ssiun2 4499 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → 𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
5 | | disjss1 4559 |
. . . . . . 7
⊢ (𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑥 ∈ 𝐵 𝐶)) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑥 ∈ 𝐵 𝐶)) |
7 | 6 | com12 32 |
. . . . 5
⊢
(Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → (𝑦 ∈ 𝐴 → Disj 𝑥 ∈ 𝐵 𝐶)) |
8 | 3, 7 | ralrimi 2940 |
. . . 4
⊢
(Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶) |
9 | 8 | a1i 11 |
. . 3
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶)) |
10 | | simplr 788 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) |
11 | | ssiun2 4499 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
12 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑢𝐵 |
13 | | nfcsb1v 3515 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦⦋𝑢 / 𝑦⦌𝐵 |
14 | | csbeq1a 3508 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑦⦌𝐵) |
15 | 12, 13, 14 | cbviun 4493 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 |
16 | 11, 15 | syl6sseqr 3615 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
17 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
18 | 17 | ad2antrl 760 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
19 | | csbeq1 3502 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑣 → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
20 | 19 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵 ↔ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵)) |
21 | 20, 16 | vtoclga 3245 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
22 | 21 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
23 | 22 | ad2antrl 760 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
24 | 12, 13, 14 | cbvdisj 4563 |
. . . . . . . . . . . . . . . 16
⊢
(Disj 𝑦
∈ 𝐴 𝐵 ↔ Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
25 | 19 | disjor 4567 |
. . . . . . . . . . . . . . . 16
⊢
(Disj 𝑢
∈ 𝐴
⦋𝑢 / 𝑦⦌𝐵 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
26 | 24, 25 | sylbb 208 |
. . . . . . . . . . . . . . 15
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
27 | | rsp2 2920 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑢 ∈
𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))) |
29 | 28 | imp 444 |
. . . . . . . . . . . . 13
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
30 | 29 | ord 391 |
. . . . . . . . . . . 12
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
31 | 30 | impr 647 |
. . . . . . . . . . 11
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) |
32 | 31 | adantlr 747 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) |
33 | | disjiun 4573 |
. . . . . . . . . 10
⊢
((Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ∧ (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵 ∧ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵 ∧ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
34 | 10, 18, 23, 32, 33 | syl13anc 1320 |
. . . . . . . . 9
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
35 | 34 | expr 641 |
. . . . . . . 8
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
36 | 35 | orrd 392 |
. . . . . . 7
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
37 | 36 | ralrimivva 2954 |
. . . . . 6
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
38 | 19 | iuneq1d 4481 |
. . . . . . 7
⊢ (𝑢 = 𝑣 → ∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) |
39 | 38 | disjor 4567 |
. . . . . 6
⊢
(Disj 𝑢
∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
40 | 37, 39 | sylibr 223 |
. . . . 5
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
41 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑢∪ 𝑥 ∈ 𝐵 𝐶 |
42 | 13, 2 | nfiun 4484 |
. . . . . 6
⊢
Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 |
43 | 14 | iuneq1d 4481 |
. . . . . 6
⊢ (𝑦 = 𝑢 → ∪
𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
44 | 41, 42, 43 | cbvdisj 4563 |
. . . . 5
⊢
(Disj 𝑦
∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
45 | 40, 44 | sylibr 223 |
. . . 4
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) |
46 | 45 | ex 449 |
. . 3
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) |
47 | 9, 46 | jcad 554 |
. 2
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))) |
48 | 15 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑟 ∈ ∪
𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
49 | | eliun 4460 |
. . . . . . . 8
⊢ (𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
50 | 48, 49 | bitri 263 |
. . . . . . 7
⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
51 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑣𝐵 |
52 | | nfcsb1v 3515 |
. . . . . . . . . 10
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐵 |
53 | | csbeq1a 3508 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → 𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
54 | 51, 52, 53 | cbviun 4493 |
. . . . . . . . 9
⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵 |
55 | 54 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑠 ∈ ∪
𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵) |
56 | | eliun 4460 |
. . . . . . . 8
⊢ (𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
57 | 55, 56 | bitri 263 |
. . . . . . 7
⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
58 | 50, 57 | anbi12i 729 |
. . . . . 6
⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
59 | | reeanv 3086 |
. . . . . 6
⊢
(∃𝑢 ∈
𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
60 | 58, 59 | bitr4i 266 |
. . . . 5
⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
61 | | simplrr 797 |
. . . . . . . . . . 11
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ¬ 𝑟 = 𝑠) |
62 | 13, 2 | nfdisj 4565 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦Disj
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 |
63 | 14 | disjeq1d 4561 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑢 → (Disj 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)) |
64 | 62, 63 | rspc 3276 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)) |
65 | 64 | impcom 445 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
66 | | disjors 4568 |
. . . . . . . . . . . . . . . . 17
⊢
(Disj 𝑥
∈ ⦋ 𝑢 /
𝑦⦌𝐵𝐶 ↔ ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
67 | 65, 66 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
68 | 67 | ad2ant2r 779 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
70 | | simplrl 796 |
. . . . . . . . . . . . . . 15
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
71 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
72 | 19 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
73 | 71, 72 | eleqtrrd 2691 |
. . . . . . . . . . . . . . 15
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
74 | 70, 73 | jca 553 |
. . . . . . . . . . . . . 14
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)) |
75 | | rsp2 2920 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑟 ∈
⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
76 | 75 | imp 444 |
. . . . . . . . . . . . . 14
⊢
((∀𝑟 ∈
⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
77 | 69, 74, 76 | syl2an2r 872 |
. . . . . . . . . . . . 13
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
78 | 77 | adantlrr 753 |
. . . . . . . . . . . 12
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
79 | 78 | ord 391 |
. . . . . . . . . . 11
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
80 | 61, 79 | mpd 15 |
. . . . . . . . . 10
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
81 | | ssiun2 4499 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪
𝑟 ∈ ⦋
𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶) |
82 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑟𝐶 |
83 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥⦋𝑟 / 𝑥⦌𝐶 |
84 | | csbeq1a 3508 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑟 → 𝐶 = ⦋𝑟 / 𝑥⦌𝐶) |
85 | 82, 83, 84 | cbviun 4493 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶 |
86 | 81, 85 | syl6sseqr 3615 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶) |
87 | | ssiun2 4499 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑠 ∈ ⦋
𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶) |
88 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑠𝐶 |
89 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐶 |
90 | | csbeq1a 3508 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑠 → 𝐶 = ⦋𝑠 / 𝑥⦌𝐶) |
91 | 88, 89, 90 | cbviun 4493 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶 = ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶 |
92 | 87, 91 | syl6sseqr 3615 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) |
93 | | ss2in 3802 |
. . . . . . . . . . . . 13
⊢
((⦋𝑟 /
𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∧ ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶)) |
94 | 86, 92, 93 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶)) |
95 | 94 | ad2antrl 760 |
. . . . . . . . . . 11
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶)) |
96 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧∪ 𝑥 ∈ 𝐵 𝐶 |
97 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐵 |
98 | 97, 2 | nfiun 4484 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 |
99 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑦⦌𝐵) |
100 | 99 | iuneq1d 4481 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → ∪
𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
101 | 96, 98, 100 | cbvdisj 4563 |
. . . . . . . . . . . . . 14
⊢
(Disj 𝑦
∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
102 | 101 | biimpi 205 |
. . . . . . . . . . . . 13
⊢
(Disj 𝑦
∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
103 | 102 | ad3antlr 763 |
. . . . . . . . . . . 12
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
104 | | simplr 788 |
. . . . . . . . . . . 12
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) |
105 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑢 ≠ 𝑣 → 𝑢 ≠ 𝑣) |
106 | | csbeq1 3502 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑢 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑢 / 𝑦⦌𝐵) |
107 | 106 | iuneq1d 4481 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑢 → ∪
𝑥 ∈ ⦋
𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
108 | | csbeq1 3502 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑣 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
109 | 108 | iuneq1d 4481 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑣 → ∪
𝑥 ∈ ⦋
𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) |
110 | 107, 109 | disji2 4569 |
. . . . . . . . . . . 12
⊢
((Disj 𝑧
∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣) → (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
111 | 103, 104,
105, 110 | syl2an3an 1378 |
. . . . . . . . . . 11
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
112 | | sseq0 3927 |
. . . . . . . . . . 11
⊢
(((⦋𝑟
/ 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) ∧ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
113 | 95, 111, 112 | syl2an2r 872 |
. . . . . . . . . 10
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
114 | 80, 113 | pm2.61dane 2869 |
. . . . . . . . 9
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
115 | 114 | expr 641 |
. . . . . . . 8
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
116 | 115 | orrd 392 |
. . . . . . 7
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
117 | 116 | ex 449 |
. . . . . 6
⊢
(((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
118 | 117 | rexlimdvva 3020 |
. . . . 5
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
119 | 60, 118 | syl5bi 231 |
. . . 4
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ((𝑟 ∈ ∪
𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
120 | 119 | ralrimivv 2953 |
. . 3
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ∀𝑟 ∈ ∪
𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
121 | | disjors 4568 |
. . 3
⊢
(Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ ∀𝑟 ∈ ∪
𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
122 | 120, 121 | sylibr 223 |
. 2
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) |
123 | 47, 122 | impbid1 214 |
1
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 ↔ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))) |