| Step | Hyp | Ref
| Expression |
| 1 | | isfi 9016 |
. . . . . . 7
⊢ (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦) |
| 2 | | ensym 9043 |
. . . . . . . . 9
⊢ (𝑥 ≈ 𝑦 → 𝑦 ≈ 𝑥) |
| 3 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ∅ → (𝑦 ≈ 𝑥 ↔ ∅ ≈ 𝑥)) |
| 4 | 3 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥))) |
| 5 | 4 | imbi1d 341 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴))) |
| 6 | 5 | albidv 1920 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴))) |
| 7 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑣 → (𝑦 ≈ 𝑥 ↔ 𝑣 ≈ 𝑥)) |
| 8 | 7 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥))) |
| 9 | 8 | imbi1d 341 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
| 10 | 9 | albidv 1920 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
| 11 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = suc 𝑣 → (𝑦 ≈ 𝑥 ↔ suc 𝑣 ≈ 𝑥)) |
| 12 | 11 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = suc 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥))) |
| 13 | 12 | imbi1d 341 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = suc 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
| 14 | 13 | albidv 1920 |
. . . . . . . . . . . . 13
⊢ (𝑦 = suc 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
| 15 | | ensym 9043 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∅
≈ 𝑥 → 𝑥 ≈
∅) |
| 16 | | en0 9058 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅) |
| 17 | 15, 16 | sylib 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅
≈ 𝑥 → 𝑥 = ∅) |
| 18 | 17 | anim1i 615 |
. . . . . . . . . . . . . . . . . 18
⊢ ((∅
≈ 𝑥 ∧ 𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅)) |
| 19 | 18 | ancoms 458 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ≠ ∅ ∧ ∅
≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅)) |
| 20 | 19 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅)) |
| 21 | | df-ne 2941 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) |
| 22 | | pm3.24 402 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
(𝑥 = ∅ ∧ ¬
𝑥 =
∅) |
| 23 | 22 | pm2.21i 119 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → ∩ 𝑥
∈ 𝐴) |
| 24 | 21, 23 | sylan2b 594 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ∩ 𝑥
∈ 𝐴) |
| 25 | 20, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴) |
| 26 | 25 | ax-gen 1795 |
. . . . . . . . . . . . . 14
⊢
∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴) |
| 27 | 26 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴)) |
| 28 | | nfv 1914 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 |
| 29 | | nfa1 2151 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) |
| 30 | | bren 8995 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑣 ≈ 𝑥 ↔ ∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥) |
| 31 | | ssel 3977 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ⊆ 𝐴 → ((𝑓‘𝑣) ∈ 𝑥 → (𝑓‘𝑣) ∈ 𝐴)) |
| 32 | | f1of 6848 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣⟶𝑥) |
| 33 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑣 ∈ V |
| 34 | 33 | sucid 6466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑣 ∈ suc 𝑣 |
| 35 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓:suc 𝑣⟶𝑥 ∧ 𝑣 ∈ suc 𝑣) → (𝑓‘𝑣) ∈ 𝑥) |
| 36 | 32, 34, 35 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓‘𝑣) ∈ 𝑥) |
| 37 | 31, 36 | impel 505 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) → (𝑓‘𝑣) ∈ 𝐴) |
| 38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴) |
| 39 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 “ 𝑣) ≠ ∅ ↔ ¬ (𝑓 “ 𝑣) = ∅) |
| 40 | | imassrn 6089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑓 “ 𝑣) ⊆ ran 𝑓 |
| 41 | | dff1o2 6853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑥)) |
| 42 | 41 | simp3bi 1148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ran 𝑓 = 𝑥) |
| 43 | 40, 42 | sseqtrid 4026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ⊆ 𝑥) |
| 44 | | sstr2 3990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑓 “ 𝑣) ⊆ 𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴)) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴)) |
| 46 | 45 | anim1d 611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅))) |
| 47 | | f1of1 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–1-1→𝑥) |
| 48 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝑥 ∈ V |
| 49 | | sssucid 6464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ 𝑣 ⊆ suc 𝑣 |
| 50 | | f1imaen2g 9055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) ∧ (𝑣 ⊆ suc 𝑣 ∧ 𝑣 ∈ V)) → (𝑓 “ 𝑣) ≈ 𝑣) |
| 51 | 49, 33, 50 | mpanr12 705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑣) ≈ 𝑣) |
| 52 | 47, 48, 51 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ≈ 𝑣) |
| 53 | 52 | ensymd 9045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑣 ≈ (𝑓 “ 𝑣)) |
| 54 | 46, 53 | jctird 526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)))) |
| 55 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑓 ∈ V |
| 56 | 55 | imaex 7936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓 “ 𝑣) ∈ V |
| 57 | | sseq1 4009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ 𝑣) ⊆ 𝐴)) |
| 58 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ≠ ∅ ↔ (𝑓 “ 𝑣) ≠ ∅)) |
| 59 | 57, 58 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = (𝑓 “ 𝑣) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ↔ ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅))) |
| 60 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑣 ≈ 𝑥 ↔ 𝑣 ≈ (𝑓 “ 𝑣))) |
| 61 | 59, 60 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 = (𝑓 “ 𝑣) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) ↔ (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)))) |
| 62 | | inteq 4949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = (𝑓 “ 𝑣) → ∩ 𝑥 = ∩
(𝑓 “ 𝑣)) |
| 63 | 62 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 = (𝑓 “ 𝑣) → (∩ 𝑥 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑣) ∈ 𝐴)) |
| 64 | 61, 63 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 = (𝑓 “ 𝑣) → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))) |
| 65 | 56, 64 | spcv 3605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴)) |
| 66 | 54, 65 | sylan9 507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ∩ (𝑓
“ 𝑣) ∈ 𝐴)) |
| 67 | | ineq1 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 = ∩
(𝑓 “ 𝑣) → (𝑧 ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ 𝑤)) |
| 68 | 67 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 = ∩
(𝑓 “ 𝑣) → ((𝑧 ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴)) |
| 69 | | ineq2 4214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 = (𝑓‘𝑣) → (∩ (𝑓 “ 𝑣) ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣))) |
| 70 | 69 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑤 = (𝑓‘𝑣) → ((∩
(𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
| 71 | 68, 70 | rspc2v 3633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((∩ (𝑓
“ 𝑣) ∈ 𝐴 ∧ (𝑓‘𝑣) ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
| 72 | 71 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (∩ (𝑓
“ 𝑣) ∈ 𝐴 → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))) |
| 73 | 66, 72 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))) |
| 74 | 73 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))) |
| 75 | 74 | exp5c 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (𝑥 ⊆ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))))) |
| 76 | 75 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ⊆ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))))) |
| 77 | 76 | imp43 427 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))) |
| 78 | 39, 77 | biimtrrid 243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (¬ (𝑓 “ 𝑣) = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))) |
| 79 | | inteq 4949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓
“ 𝑣) = ∩ ∅) |
| 80 | | int0 4962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ∩ ∅ = V |
| 81 | 79, 80 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓
“ 𝑣) =
V) |
| 82 | 81 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) = (V ∩ (𝑓‘𝑣))) |
| 83 | | ssv 4008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓‘𝑣) ⊆ V |
| 84 | | sseqin2 4223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓‘𝑣) ⊆ V ↔ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣)) |
| 85 | 83, 84 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (V ∩
(𝑓‘𝑣)) = (𝑓‘𝑣) |
| 86 | 82, 85 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) = (𝑓‘𝑣)) |
| 87 | 86 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 “ 𝑣) = ∅ → ((∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ (𝑓‘𝑣) ∈ 𝐴)) |
| 88 | 87 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓 “ 𝑣) = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
| 89 | 78, 88 | pm2.61d2 181 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
| 90 | 38, 89 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (∩
(𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴) |
| 91 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓‘𝑣) ∈ V |
| 92 | 91 | intunsn 4987 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∩ ((𝑓
“ 𝑣) ∪ {(𝑓‘𝑣)}) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) |
| 93 | | f1ofn 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓 Fn suc 𝑣) |
| 94 | | fnsnfv 6988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑓 Fn suc 𝑣 ∧ 𝑣 ∈ suc 𝑣) → {(𝑓‘𝑣)} = (𝑓 “ {𝑣})) |
| 95 | 93, 34, 94 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → {(𝑓‘𝑣)} = (𝑓 “ {𝑣})) |
| 96 | 95 | uneq2d 4168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣}))) |
| 97 | | df-suc 6390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ suc 𝑣 = (𝑣 ∪ {𝑣}) |
| 98 | 97 | imaeq2i 6076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣})) |
| 99 | | imaundi 6169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})) |
| 100 | 98, 99 | eqtr2i 2766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣) |
| 101 | 96, 100 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (𝑓 “ suc 𝑣)) |
| 102 | | f1ofo 6855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–onto→𝑥) |
| 103 | | foima 6825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:suc 𝑣–onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥) |
| 104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥) |
| 105 | 101, 104 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = 𝑥) |
| 106 | 105 | inteqd 4951 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ∩ ((𝑓
“ 𝑣) ∪ {(𝑓‘𝑣)}) = ∩ 𝑥) |
| 107 | 92, 106 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) = ∩ 𝑥) |
| 108 | 107 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴)) |
| 109 | 108 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((∩
(𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴)) |
| 110 | 90, 109 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ∩ 𝑥 ∈ 𝐴) |
| 111 | 110 | exp43 436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ⊆ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
| 112 | 111 | exlimdv 1933 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ⊆ 𝐴 → (∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
| 113 | 30, 112 | biimtrid 242 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ⊆ 𝐴 → (suc 𝑣 ≈ 𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
| 114 | 113 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ⊆ 𝐴 ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))) |
| 115 | 114 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))) |
| 116 | 115 | com13 88 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
| 117 | 28, 29, 116 | alrimd 2215 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
| 118 | 117 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ω →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))) |
| 119 | 6, 10, 14, 27, 118 | finds2 7920 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
| 120 | | sp 2183 |
. . . . . . . . . . . 12
⊢
(∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) |
| 121 | 119, 120 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
| 122 | 121 | exp4a 431 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑦 ≈ 𝑥 → ∩ 𝑥 ∈ 𝐴)))) |
| 123 | 122 | com24 95 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → (𝑦 ≈ 𝑥 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
| 124 | 2, 123 | syl5 34 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → (𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
| 125 | 124 | rexlimiv 3148 |
. . . . . . 7
⊢
(∃𝑦 ∈
ω 𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))) |
| 126 | 1, 125 | sylbi 217 |
. . . . . 6
⊢ (𝑥 ∈ Fin → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))) |
| 127 | 126 | com13 88 |
. . . . 5
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑥 ∈ Fin → ∩ 𝑥
∈ 𝐴))) |
| 128 | 127 | impd 410 |
. . . 4
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |
| 129 | 128 | alrimiv 1927 |
. . 3
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |
| 130 | | zfpair2 5433 |
. . . . . 6
⊢ {𝑧, 𝑤} ∈ V |
| 131 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑥 = {𝑧, 𝑤} → (𝑥 ⊆ 𝐴 ↔ {𝑧, 𝑤} ⊆ 𝐴)) |
| 132 | | neeq1 3003 |
. . . . . . . . 9
⊢ (𝑥 = {𝑧, 𝑤} → (𝑥 ≠ ∅ ↔ {𝑧, 𝑤} ≠ ∅)) |
| 133 | 131, 132 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑥 = {𝑧, 𝑤} → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ↔ ({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅))) |
| 134 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑥 = {𝑧, 𝑤} → (𝑥 ∈ Fin ↔ {𝑧, 𝑤} ∈ Fin)) |
| 135 | 133, 134 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = {𝑧, 𝑤} → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) ↔ (({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin))) |
| 136 | | inteq 4949 |
. . . . . . . 8
⊢ (𝑥 = {𝑧, 𝑤} → ∩ 𝑥 = ∩
{𝑧, 𝑤}) |
| 137 | 136 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = {𝑧, 𝑤} → (∩ 𝑥 ∈ 𝐴 ↔ ∩ {𝑧, 𝑤} ∈ 𝐴)) |
| 138 | 135, 137 | imbi12d 344 |
. . . . . 6
⊢ (𝑥 = {𝑧, 𝑤} → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴) ↔ ((({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin) → ∩ {𝑧,
𝑤} ∈ 𝐴))) |
| 139 | 130, 138 | spcv 3605 |
. . . . 5
⊢
(∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴) → ((({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin) → ∩ {𝑧,
𝑤} ∈ 𝐴)) |
| 140 | | vex 3484 |
. . . . . . 7
⊢ 𝑧 ∈ V |
| 141 | | vex 3484 |
. . . . . . 7
⊢ 𝑤 ∈ V |
| 142 | 140, 141 | prss 4820 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ↔ {𝑧, 𝑤} ⊆ 𝐴) |
| 143 | 140 | prnz 4777 |
. . . . . . 7
⊢ {𝑧, 𝑤} ≠ ∅ |
| 144 | 143 | biantru 529 |
. . . . . 6
⊢ ({𝑧, 𝑤} ⊆ 𝐴 ↔ ({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅)) |
| 145 | | prfi 9363 |
. . . . . . 7
⊢ {𝑧, 𝑤} ∈ Fin |
| 146 | 145 | biantru 529 |
. . . . . 6
⊢ (({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ↔ (({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin)) |
| 147 | 142, 144,
146 | 3bitrri 298 |
. . . . 5
⊢ ((({𝑧, 𝑤} ⊆ 𝐴 ∧ {𝑧, 𝑤} ≠ ∅) ∧ {𝑧, 𝑤} ∈ Fin) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) |
| 148 | 140, 141 | intpr 4982 |
. . . . . 6
⊢ ∩ {𝑧,
𝑤} = (𝑧 ∩ 𝑤) |
| 149 | 148 | eleq1i 2832 |
. . . . 5
⊢ (∩ {𝑧,
𝑤} ∈ 𝐴 ↔ (𝑧 ∩ 𝑤) ∈ 𝐴) |
| 150 | 139, 147,
149 | 3imtr3g 295 |
. . . 4
⊢
(∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴) → ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ∩ 𝑤) ∈ 𝐴)) |
| 151 | 150 | ralrimivv 3200 |
. . 3
⊢
(∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴) →
∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) |
| 152 | 129, 151 | impbii 209 |
. 2
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |
| 153 | | ineq1 4213 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝑥 ∩ 𝑦) = (𝑧 ∩ 𝑦)) |
| 154 | 153 | eleq1d 2826 |
. . 3
⊢ (𝑥 = 𝑧 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑦) ∈ 𝐴)) |
| 155 | | ineq2 4214 |
. . . 4
⊢ (𝑦 = 𝑤 → (𝑧 ∩ 𝑦) = (𝑧 ∩ 𝑤)) |
| 156 | 155 | eleq1d 2826 |
. . 3
⊢ (𝑦 = 𝑤 → ((𝑧 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑤) ∈ 𝐴)) |
| 157 | 154, 156 | cbvral2vw 3241 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) |
| 158 | | df-3an 1089 |
. . . 4
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin)) |
| 159 | 158 | imbi1i 349 |
. . 3
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |
| 160 | 159 | albii 1819 |
. 2
⊢
(∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴) ↔
∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |
| 161 | 152, 157,
160 | 3bitr4i 303 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |