Proof of Theorem fnejoin2
Step | Hyp | Ref
| Expression |
1 | | unisng 4388 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑉 → ∪ {𝑋} = 𝑋) |
2 | 1 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑋 = ∪ {𝑋}) |
3 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → 𝑋 = ∪ {𝑋}) |
4 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑆 = ∅ → if(𝑆 = ∅, {𝑋}, ∪ 𝑆) = {𝑋}) |
5 | 4 | unieqd 4382 |
. . . . . . . 8
⊢ (𝑆 = ∅ → ∪ if(𝑆
= ∅, {𝑋}, ∪ 𝑆) =
∪ {𝑋}) |
6 | 5 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑆 = ∅ → (𝑋 = ∪
if(𝑆 = ∅, {𝑋}, ∪
𝑆) ↔ 𝑋 = ∪ {𝑋})) |
7 | 3, 6 | syl5ibrcom 236 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (𝑆 = ∅ → 𝑋 = ∪ if(𝑆 = ∅, {𝑋}, ∪ 𝑆))) |
8 | | n0 3890 |
. . . . . . 7
⊢ (𝑆 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑆) |
9 | | unieq 4380 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ∪ 𝑦 = ∪
𝑥) |
10 | 9 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑥)) |
11 | 10 | rspccva 3281 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆) → 𝑋 = ∪ 𝑥) |
12 | 11 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆) → 𝑋 = ∪ 𝑥) |
13 | | fnejoin1 31533 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆) → 𝑥Fneif(𝑆 = ∅, {𝑋}, ∪ 𝑆)) |
14 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 =
∪ 𝑥 |
15 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ if(𝑆
= ∅, {𝑋}, ∪ 𝑆) =
∪ if(𝑆 = ∅, {𝑋}, ∪ 𝑆) |
16 | 14, 15 | fnebas 31509 |
. . . . . . . . . . 11
⊢ (𝑥Fneif(𝑆 = ∅, {𝑋}, ∪ 𝑆) → ∪ 𝑥 =
∪ if(𝑆 = ∅, {𝑋}, ∪ 𝑆)) |
17 | 13, 16 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆) → ∪ 𝑥 = ∪
if(𝑆 = ∅, {𝑋}, ∪
𝑆)) |
18 | 12, 17 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆) → 𝑋 = ∪ if(𝑆 = ∅, {𝑋}, ∪ 𝑆)) |
19 | 18 | 3expia 1259 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (𝑥 ∈ 𝑆 → 𝑋 = ∪ if(𝑆 = ∅, {𝑋}, ∪ 𝑆))) |
20 | 19 | exlimdv 1848 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (∃𝑥 𝑥 ∈ 𝑆 → 𝑋 = ∪ if(𝑆 = ∅, {𝑋}, ∪ 𝑆))) |
21 | 8, 20 | syl5bi 231 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (𝑆 ≠ ∅ → 𝑋 = ∪ if(𝑆 = ∅, {𝑋}, ∪ 𝑆))) |
22 | 7, 21 | pm2.61dne 2868 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → 𝑋 = ∪ if(𝑆 = ∅, {𝑋}, ∪ 𝑆)) |
23 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝑇 =
∪ 𝑇 |
24 | 15, 23 | fnebas 31509 |
. . . . 5
⊢ (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 → ∪
if(𝑆 = ∅, {𝑋}, ∪
𝑆) = ∪ 𝑇) |
25 | 22, 24 | sylan9eq 2664 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇) → 𝑋 = ∪ 𝑇) |
26 | 25 | ex 449 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 → 𝑋 = ∪ 𝑇)) |
27 | | fnetr 31516 |
. . . . . . 7
⊢ ((𝑥Fneif(𝑆 = ∅, {𝑋}, ∪ 𝑆) ∧ if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇) → 𝑥Fne𝑇) |
28 | 27 | ex 449 |
. . . . . 6
⊢ (𝑥Fneif(𝑆 = ∅, {𝑋}, ∪ 𝑆) → (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 → 𝑥Fne𝑇)) |
29 | 13, 28 | syl 17 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆) → (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 → 𝑥Fne𝑇)) |
30 | 29 | 3expa 1257 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ 𝑥 ∈ 𝑆) → (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 → 𝑥Fne𝑇)) |
31 | 30 | ralrimdva 2952 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 → ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) |
32 | 26, 31 | jcad 554 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 → (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇))) |
33 | 22 | adantr 480 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → 𝑋 = ∪ if(𝑆 = ∅, {𝑋}, ∪ 𝑆)) |
34 | | simprl 790 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → 𝑋 = ∪ 𝑇) |
35 | 33, 34 | eqtr3d 2646 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → ∪
if(𝑆 = ∅, {𝑋}, ∪
𝑆) = ∪ 𝑇) |
36 | | sseq1 3589 |
. . . . 5
⊢ ({𝑋} = if(𝑆 = ∅, {𝑋}, ∪ 𝑆) → ({𝑋} ⊆ (topGen‘𝑇) ↔ if(𝑆 = ∅, {𝑋}, ∪ 𝑆) ⊆ (topGen‘𝑇))) |
37 | | sseq1 3589 |
. . . . 5
⊢ (∪ 𝑆 =
if(𝑆 = ∅, {𝑋}, ∪
𝑆) → (∪ 𝑆
⊆ (topGen‘𝑇)
↔ if(𝑆 = ∅,
{𝑋}, ∪ 𝑆)
⊆ (topGen‘𝑇))) |
38 | | elex 3185 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ V) |
39 | 38 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → 𝑋 ∈ V) |
40 | 34, 39 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → ∪ 𝑇 ∈ V) |
41 | | uniexb 6866 |
. . . . . . . . . 10
⊢ (𝑇 ∈ V ↔ ∪ 𝑇
∈ V) |
42 | 40, 41 | sylibr 223 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → 𝑇 ∈ V) |
43 | | ssid 3587 |
. . . . . . . . 9
⊢ 𝑇 ⊆ 𝑇 |
44 | | eltg3i 20576 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑇 ⊆ 𝑇) → ∪ 𝑇 ∈ (topGen‘𝑇)) |
45 | 42, 43, 44 | sylancl 693 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → ∪ 𝑇 ∈ (topGen‘𝑇)) |
46 | 34, 45 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → 𝑋 ∈ (topGen‘𝑇)) |
47 | 46 | snssd 4281 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → {𝑋} ⊆ (topGen‘𝑇)) |
48 | 47 | adantr 480 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) ∧ 𝑆 = ∅) → {𝑋} ⊆ (topGen‘𝑇)) |
49 | | simplrr 797 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) ∧ ¬ 𝑆 = ∅) → ∀𝑥 ∈ 𝑆 𝑥Fne𝑇) |
50 | | fnetg 31510 |
. . . . . . . 8
⊢ (𝑥Fne𝑇 → 𝑥 ⊆ (topGen‘𝑇)) |
51 | 50 | ralimi 2936 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑆 𝑥Fne𝑇 → ∀𝑥 ∈ 𝑆 𝑥 ⊆ (topGen‘𝑇)) |
52 | 49, 51 | syl 17 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) ∧ ¬ 𝑆 = ∅) → ∀𝑥 ∈ 𝑆 𝑥 ⊆ (topGen‘𝑇)) |
53 | | unissb 4405 |
. . . . . 6
⊢ (∪ 𝑆
⊆ (topGen‘𝑇)
↔ ∀𝑥 ∈
𝑆 𝑥 ⊆ (topGen‘𝑇)) |
54 | 52, 53 | sylibr 223 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) ∧ ¬ 𝑆 = ∅) → ∪ 𝑆
⊆ (topGen‘𝑇)) |
55 | 36, 37, 48, 54 | ifbothda 4073 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → if(𝑆 = ∅, {𝑋}, ∪ 𝑆) ⊆ (topGen‘𝑇)) |
56 | 15, 23 | isfne4 31505 |
. . . 4
⊢ (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 ↔ (∪
if(𝑆 = ∅, {𝑋}, ∪
𝑆) = ∪ 𝑇
∧ if(𝑆 = ∅,
{𝑋}, ∪ 𝑆)
⊆ (topGen‘𝑇))) |
57 | 35, 55, 56 | sylanbrc 695 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) ∧ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)) → if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇) |
58 | 57 | ex 449 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → ((𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇) → if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇)) |
59 | 32, 58 | impbid 201 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 ↔ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇))) |