Step | Hyp | Ref
| Expression |
1 | | nfiu1 4959 |
. . . . . 6
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐴 𝐵 |
2 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑦𝐶 |
3 | 1, 2 | nfdisjw 5051 |
. . . . 5
⊢
Ⅎ𝑦Disj
𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 |
4 | | disjss1 5045 |
. . . . . 6
⊢ (𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑥 ∈ 𝐵 𝐶)) |
5 | | ssiun2 4977 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → 𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
6 | 4, 5 | syl11 33 |
. . . . 5
⊢
(Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → (𝑦 ∈ 𝐴 → Disj 𝑥 ∈ 𝐵 𝐶)) |
7 | 3, 6 | ralrimi 3140 |
. . . 4
⊢
(Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶) |
8 | 7 | a1i 11 |
. . 3
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶)) |
9 | | simplr 766 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) |
10 | | ssiun2 4977 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
11 | | nfcv 2907 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑢𝐵 |
12 | | nfcsb1v 3857 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦⦋𝑢 / 𝑦⦌𝐵 |
13 | | csbeq1a 3846 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑦⦌𝐵) |
14 | 11, 12, 13 | cbviun 4966 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 |
15 | 10, 14 | sseqtrrdi 3972 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
16 | 15 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
17 | 16 | ad2antrl 725 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
18 | | csbeq1 3835 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑣 → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
19 | 18 | sseq1d 3952 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵 ↔ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵)) |
20 | 19, 15 | vtoclga 3511 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
21 | 20 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
22 | 21 | ad2antrl 725 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵) |
23 | 11, 12, 13 | cbvdisj 5049 |
. . . . . . . . . . . . . . . 16
⊢
(Disj 𝑦
∈ 𝐴 𝐵 ↔ Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
24 | 18 | disjor 5054 |
. . . . . . . . . . . . . . . 16
⊢
(Disj 𝑢
∈ 𝐴
⦋𝑢 / 𝑦⦌𝐵 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
25 | 23, 24 | sylbb 218 |
. . . . . . . . . . . . . . 15
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
26 | | rsp2 3137 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑢 ∈
𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))) |
28 | 27 | imp 407 |
. . . . . . . . . . . . 13
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
29 | 28 | ord 861 |
. . . . . . . . . . . 12
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) |
30 | 29 | impr 455 |
. . . . . . . . . . 11
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) |
31 | 30 | adantlr 712 |
. . . . . . . . . 10
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) |
32 | | disjiun 5061 |
. . . . . . . . . 10
⊢
((Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ∧ (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵 ∧ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪
𝑦 ∈ 𝐴 𝐵 ∧ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
33 | 9, 17, 22, 31, 32 | syl13anc 1371 |
. . . . . . . . 9
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
34 | 33 | expr 457 |
. . . . . . . 8
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
35 | 34 | orrd 860 |
. . . . . . 7
⊢
(((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
36 | 35 | ralrimivva 3120 |
. . . . . 6
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
37 | 18 | iuneq1d 4952 |
. . . . . . 7
⊢ (𝑢 = 𝑣 → ∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) |
38 | 37 | disjor 5054 |
. . . . . 6
⊢
(Disj 𝑢
∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅)) |
39 | 36, 38 | sylibr 233 |
. . . . 5
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
40 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑢∪ 𝑥 ∈ 𝐵 𝐶 |
41 | 12, 2 | nfiun 4955 |
. . . . . 6
⊢
Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 |
42 | 13 | iuneq1d 4952 |
. . . . . 6
⊢ (𝑦 = 𝑢 → ∪
𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
43 | 40, 41, 42 | cbvdisj 5049 |
. . . . 5
⊢
(Disj 𝑦
∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
44 | 39, 43 | sylibr 233 |
. . . 4
⊢
((Disj 𝑦
∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) |
45 | 44 | ex 413 |
. . 3
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)) |
46 | 8, 45 | jcad 513 |
. 2
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))) |
47 | 14 | eleq2i 2830 |
. . . . . . . 8
⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑟 ∈ ∪
𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵) |
48 | | eliun 4929 |
. . . . . . . 8
⊢ (𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
49 | 47, 48 | bitri 274 |
. . . . . . 7
⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
50 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑣𝐵 |
51 | | nfcsb1v 3857 |
. . . . . . . . . 10
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐵 |
52 | | csbeq1a 3846 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → 𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
53 | 50, 51, 52 | cbviun 4966 |
. . . . . . . . 9
⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵 |
54 | 53 | eleq2i 2830 |
. . . . . . . 8
⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑠 ∈ ∪
𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵) |
55 | | eliun 4929 |
. . . . . . . 8
⊢ (𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
56 | 54, 55 | bitri 274 |
. . . . . . 7
⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
57 | 49, 56 | anbi12i 627 |
. . . . . 6
⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
58 | | reeanv 3292 |
. . . . . 6
⊢
(∃𝑢 ∈
𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
59 | 57, 58 | bitr4i 277 |
. . . . 5
⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) |
60 | | simplrr 775 |
. . . . . . . . . . 11
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ¬ 𝑟 = 𝑠) |
61 | 12, 2 | nfdisjw 5051 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦Disj
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 |
62 | 13 | disjeq1d 5047 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑢 → (Disj 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)) |
63 | 61, 62 | rspc 3547 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)) |
64 | 63 | impcom 408 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
65 | | disjors 5055 |
. . . . . . . . . . . . . . . . 17
⊢
(Disj 𝑥
∈ ⦋ 𝑢 /
𝑦⦌𝐵𝐶 ↔ ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
66 | 64, 65 | sylib 217 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
67 | 66 | ad2ant2r 744 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
68 | 67 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
69 | | simplrl 774 |
. . . . . . . . . . . . . . 15
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
70 | | simplrr 775 |
. . . . . . . . . . . . . . . 16
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) |
71 | 18 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
72 | 70, 71 | eleqtrrd 2842 |
. . . . . . . . . . . . . . 15
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵) |
73 | 69, 72 | jca 512 |
. . . . . . . . . . . . . 14
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)) |
74 | | rsp2 3137 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑟 ∈
⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
75 | 74 | imp 407 |
. . . . . . . . . . . . . 14
⊢
((∀𝑟 ∈
⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
76 | 68, 73, 75 | syl2an2r 682 |
. . . . . . . . . . . . 13
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
77 | 76 | adantlrr 718 |
. . . . . . . . . . . 12
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
78 | 77 | ord 861 |
. . . . . . . . . . 11
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
79 | 60, 78 | mpd 15 |
. . . . . . . . . 10
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
80 | | ssiun2 4977 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪
𝑟 ∈ ⦋
𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶) |
81 | | nfcv 2907 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑟𝐶 |
82 | | nfcsb1v 3857 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥⦋𝑟 / 𝑥⦌𝐶 |
83 | | csbeq1a 3846 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑟 → 𝐶 = ⦋𝑟 / 𝑥⦌𝐶) |
84 | 81, 82, 83 | cbviun 4966 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶 |
85 | 80, 84 | sseqtrrdi 3972 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶) |
86 | | ssiun2 4977 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑠 ∈ ⦋
𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶) |
87 | | nfcv 2907 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑠𝐶 |
88 | | nfcsb1v 3857 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐶 |
89 | | csbeq1a 3846 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑠 → 𝐶 = ⦋𝑠 / 𝑥⦌𝐶) |
90 | 87, 88, 89 | cbviun 4966 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶 = ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶 |
91 | 86, 90 | sseqtrrdi 3972 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) |
92 | | ss2in 4171 |
. . . . . . . . . . . . 13
⊢
((⦋𝑟 /
𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∧ ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶)) |
93 | 85, 91, 92 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶)) |
94 | 93 | ad2antrl 725 |
. . . . . . . . . . 11
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶)) |
95 | | nfcv 2907 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧∪ 𝑥 ∈ 𝐵 𝐶 |
96 | | nfcsb1v 3857 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐵 |
97 | 96, 2 | nfiun 4955 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 |
98 | | csbeq1a 3846 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑦⦌𝐵) |
99 | 98 | iuneq1d 4952 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → ∪
𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
100 | 95, 97, 99 | cbvdisj 5049 |
. . . . . . . . . . . . . 14
⊢
(Disj 𝑦
∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
101 | 100 | biimpi 215 |
. . . . . . . . . . . . 13
⊢
(Disj 𝑦
∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
102 | 101 | ad3antlr 728 |
. . . . . . . . . . . 12
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶) |
103 | | simplr 766 |
. . . . . . . . . . . 12
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) |
104 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑢 ≠ 𝑣 → 𝑢 ≠ 𝑣) |
105 | | csbeq1 3835 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑢 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑢 / 𝑦⦌𝐵) |
106 | 105 | iuneq1d 4952 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑢 → ∪
𝑥 ∈ ⦋
𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶) |
107 | | csbeq1 3835 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑣 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵) |
108 | 107 | iuneq1d 4952 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑣 → ∪
𝑥 ∈ ⦋
𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) |
109 | 106, 108 | disji2 5056 |
. . . . . . . . . . . 12
⊢
((Disj 𝑧
∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣) → (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
110 | 102, 103,
104, 109 | syl2an3an 1421 |
. . . . . . . . . . 11
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) |
111 | | sseq0 4334 |
. . . . . . . . . . 11
⊢
(((⦋𝑟
/ 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) ∧ (∪
𝑥 ∈ ⦋
𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪
𝑥 ∈ ⦋
𝑣 / 𝑦⦌𝐵𝐶) = ∅) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
112 | 94, 110, 111 | syl2an2r 682 |
. . . . . . . . . 10
⊢
(((((∀𝑦
∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
113 | 79, 112 | pm2.61dane 3032 |
. . . . . . . . 9
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) |
114 | 113 | expr 457 |
. . . . . . . 8
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
115 | 114 | orrd 860 |
. . . . . . 7
⊢
((((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
116 | 115 | ex 413 |
. . . . . 6
⊢
(((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
117 | 116 | rexlimdvva 3221 |
. . . . 5
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
118 | 59, 117 | syl5bi 241 |
. . . 4
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ((𝑟 ∈ ∪
𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))) |
119 | 118 | ralrimivv 3119 |
. . 3
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ∀𝑟 ∈ ∪
𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
120 | | disjors 5055 |
. . 3
⊢
(Disj 𝑥
∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ ∀𝑟 ∈ ∪
𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪
𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)) |
121 | 119, 120 | sylibr 233 |
. 2
⊢
((∀𝑦 ∈
𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶) |
122 | 46, 121 | impbid1 224 |
1
⊢
(Disj 𝑦
∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪
𝑦 ∈ 𝐴 𝐵𝐶 ↔ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))) |