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