| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . 5
⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅)) |
| 2 | 1 | neeq1d 3000 |
. . . 4
⊢ (𝑣 = ∅ → ((𝐹‘𝑣) ≠ 𝑥 ↔ (𝐹‘∅) ≠ 𝑥)) |
| 3 | 2 | imbi2d 340 |
. . 3
⊢ (𝑣 = ∅ → (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐹‘𝑣) ≠ 𝑥) ↔ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘∅) ≠ 𝑥))) |
| 4 | | fveq2 6906 |
. . . . 5
⊢ (𝑣 = 𝑢 → (𝐹‘𝑣) = (𝐹‘𝑢)) |
| 5 | 4 | neeq1d 3000 |
. . . 4
⊢ (𝑣 = 𝑢 → ((𝐹‘𝑣) ≠ 𝑥 ↔ (𝐹‘𝑢) ≠ 𝑥)) |
| 6 | 5 | imbi2d 340 |
. . 3
⊢ (𝑣 = 𝑢 → (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘𝑣) ≠ 𝑥) ↔ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘𝑢) ≠ 𝑥))) |
| 7 | | fveq2 6906 |
. . . . 5
⊢ (𝑣 = suc 𝑢 → (𝐹‘𝑣) = (𝐹‘suc 𝑢)) |
| 8 | 7 | neeq1d 3000 |
. . . 4
⊢ (𝑣 = suc 𝑢 → ((𝐹‘𝑣) ≠ 𝑥 ↔ (𝐹‘suc 𝑢) ≠ 𝑥)) |
| 9 | 8 | imbi2d 340 |
. . 3
⊢ (𝑣 = suc 𝑢 → (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘𝑣) ≠ 𝑥) ↔ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘suc 𝑢) ≠ 𝑥))) |
| 10 | | fveq2 6906 |
. . . . 5
⊢ (𝑣 = 𝐴 → (𝐹‘𝑣) = (𝐹‘𝐴)) |
| 11 | 10 | neeq1d 3000 |
. . . 4
⊢ (𝑣 = 𝐴 → ((𝐹‘𝑣) ≠ 𝑥 ↔ (𝐹‘𝐴) ≠ 𝑥)) |
| 12 | 11 | imbi2d 340 |
. . 3
⊢ (𝑣 = 𝐴 → (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘𝑣) ≠ 𝑥) ↔ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘𝐴) ≠ 𝑥))) |
| 13 | | inf3lem.1 |
. . . . . . . 8
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) |
| 14 | | inf3lem.2 |
. . . . . . . 8
⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) |
| 15 | | inf3lem.3 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
| 16 | | inf3lem.4 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
| 17 | 13, 14, 15, 16 | inf3lemb 9665 |
. . . . . . 7
⊢ (𝐹‘∅) =
∅ |
| 18 | 17 | eqeq1i 2742 |
. . . . . 6
⊢ ((𝐹‘∅) = 𝑥 ↔ ∅ = 𝑥) |
| 19 | | eqcom 2744 |
. . . . . 6
⊢ (∅
= 𝑥 ↔ 𝑥 = ∅) |
| 20 | 18, 19 | sylbb 219 |
. . . . 5
⊢ ((𝐹‘∅) = 𝑥 → 𝑥 = ∅) |
| 21 | 20 | necon3i 2973 |
. . . 4
⊢ (𝑥 ≠ ∅ → (𝐹‘∅) ≠ 𝑥) |
| 22 | 21 | adantr 480 |
. . 3
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐹‘∅)
≠ 𝑥) |
| 23 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑢 ∈ V |
| 24 | 13, 14, 23, 16 | inf3lemd 9667 |
. . . . . . . 8
⊢ (𝑢 ∈ ω → (𝐹‘𝑢) ⊆ 𝑥) |
| 25 | | df-pss 3971 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑢) ⊊ 𝑥 ↔ ((𝐹‘𝑢) ⊆ 𝑥 ∧ (𝐹‘𝑢) ≠ 𝑥)) |
| 26 | | pssnel 4471 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑢) ⊊ 𝑥 → ∃𝑣(𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ (𝐹‘𝑢))) |
| 27 | 25, 26 | sylbir 235 |
. . . . . . . . 9
⊢ (((𝐹‘𝑢) ⊆ 𝑥 ∧ (𝐹‘𝑢) ≠ 𝑥) → ∃𝑣(𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ (𝐹‘𝑢))) |
| 28 | | ssel 3977 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ ∪ 𝑥
→ (𝑣 ∈ 𝑥 → 𝑣 ∈ ∪ 𝑥)) |
| 29 | | eluni 4910 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ ∪ 𝑥
↔ ∃𝑓(𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥)) |
| 30 | 28, 29 | imbitrdi 251 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ∪ 𝑥
→ (𝑣 ∈ 𝑥 → ∃𝑓(𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥))) |
| 31 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘suc 𝑢) = 𝑥 → (𝑓 ∈ (𝐹‘suc 𝑢) ↔ 𝑓 ∈ 𝑥)) |
| 32 | 31 | biimparc 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ 𝑥 ∧ (𝐹‘suc 𝑢) = 𝑥) → 𝑓 ∈ (𝐹‘suc 𝑢)) |
| 33 | 13, 14, 23, 16 | inf3lemc 9666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ ω → (𝐹‘suc 𝑢) = (𝐺‘(𝐹‘𝑢))) |
| 34 | 33 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ ω → (𝑓 ∈ (𝐹‘suc 𝑢) ↔ 𝑓 ∈ (𝐺‘(𝐹‘𝑢)))) |
| 35 | | elin 3967 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ (𝑓 ∩ 𝑥) ↔ (𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥)) |
| 36 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑓 ∈ V |
| 37 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹‘𝑢) ∈ V |
| 38 | 13, 14, 36, 37 | inf3lema 9664 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 ∈ (𝐺‘(𝐹‘𝑢)) ↔ (𝑓 ∈ 𝑥 ∧ (𝑓 ∩ 𝑥) ⊆ (𝐹‘𝑢))) |
| 39 | 38 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ (𝐺‘(𝐹‘𝑢)) → (𝑓 ∩ 𝑥) ⊆ (𝐹‘𝑢)) |
| 40 | 39 | sseld 3982 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ (𝐺‘(𝐹‘𝑢)) → (𝑣 ∈ (𝑓 ∩ 𝑥) → 𝑣 ∈ (𝐹‘𝑢))) |
| 41 | 35, 40 | biimtrrid 243 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ (𝐺‘(𝐹‘𝑢)) → ((𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ (𝐹‘𝑢))) |
| 42 | 34, 41 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ω → (𝑓 ∈ (𝐹‘suc 𝑢) → ((𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ (𝐹‘𝑢)))) |
| 43 | 32, 42 | syl5 34 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ω → ((𝑓 ∈ 𝑥 ∧ (𝐹‘suc 𝑢) = 𝑥) → ((𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ (𝐹‘𝑢)))) |
| 44 | 43 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ω → ((𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥) → ((𝑓 ∈ 𝑥 ∧ (𝐹‘suc 𝑢) = 𝑥) → 𝑣 ∈ (𝐹‘𝑢)))) |
| 45 | 44 | exp5c 444 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ω → (𝑣 ∈ 𝑓 → (𝑣 ∈ 𝑥 → (𝑓 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢)))))) |
| 46 | 45 | com34 91 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ω → (𝑣 ∈ 𝑓 → (𝑓 ∈ 𝑥 → (𝑣 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢)))))) |
| 47 | 46 | impd 410 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ω → ((𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥) → (𝑣 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢))))) |
| 48 | 47 | exlimdv 1933 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ω →
(∃𝑓(𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥) → (𝑣 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢))))) |
| 49 | 30, 48 | sylan9r 508 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝑣 ∈ 𝑥 → (𝑣 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢))))) |
| 50 | 49 | pm2.43d 53 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝑣 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢)))) |
| 51 | | id 22 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢)) → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢))) |
| 52 | 51 | necon3bd 2954 |
. . . . . . . . . . . 12
⊢ (((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢)) → (¬ 𝑣 ∈ (𝐹‘𝑢) → (𝐹‘suc 𝑢) ≠ 𝑥)) |
| 53 | 50, 52 | syl6 35 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝑣 ∈ 𝑥 → (¬ 𝑣 ∈ (𝐹‘𝑢) → (𝐹‘suc 𝑢) ≠ 𝑥))) |
| 54 | 53 | impd 410 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ (𝐹‘𝑢)) → (𝐹‘suc 𝑢) ≠ 𝑥)) |
| 55 | 54 | exlimdv 1933 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ (∃𝑣(𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ (𝐹‘𝑢)) → (𝐹‘suc 𝑢) ≠ 𝑥)) |
| 56 | 27, 55 | syl5 34 |
. . . . . . . 8
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ (((𝐹‘𝑢) ⊆ 𝑥 ∧ (𝐹‘𝑢) ≠ 𝑥) → (𝐹‘suc 𝑢) ≠ 𝑥)) |
| 57 | 24, 56 | sylani 604 |
. . . . . . 7
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝑢 ∈ ω
∧ (𝐹‘𝑢) ≠ 𝑥) → (𝐹‘suc 𝑢) ≠ 𝑥)) |
| 58 | 57 | exp4b 430 |
. . . . . 6
⊢ (𝑢 ∈ ω → (𝑥 ⊆ ∪ 𝑥
→ (𝑢 ∈ ω
→ ((𝐹‘𝑢) ≠ 𝑥 → (𝐹‘suc 𝑢) ≠ 𝑥)))) |
| 59 | 58 | pm2.43a 54 |
. . . . 5
⊢ (𝑢 ∈ ω → (𝑥 ⊆ ∪ 𝑥
→ ((𝐹‘𝑢) ≠ 𝑥 → (𝐹‘suc 𝑢) ≠ 𝑥))) |
| 60 | 59 | adantld 490 |
. . . 4
⊢ (𝑢 ∈ ω → ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝐹‘𝑢) ≠ 𝑥 → (𝐹‘suc 𝑢) ≠ 𝑥))) |
| 61 | 60 | a2d 29 |
. . 3
⊢ (𝑢 ∈ ω → (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐹‘𝑢) ≠ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘suc 𝑢) ≠ 𝑥))) |
| 62 | 3, 6, 9, 12, 22, 61 | finds 7918 |
. 2
⊢ (𝐴 ∈ ω → ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐹‘𝐴) ≠ 𝑥)) |
| 63 | 62 | com12 32 |
1
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐴 ∈ ω
→ (𝐹‘𝐴) ≠ 𝑥)) |