Step | Hyp | Ref
| Expression |
1 | | fveq2 6717 |
. . . . 5
⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅)) |
2 | 1 | neeq1d 3000 |
. . . 4
⊢ (𝑣 = ∅ → ((𝐹‘𝑣) ≠ 𝑥 ↔ (𝐹‘∅) ≠ 𝑥)) |
3 | 2 | imbi2d 344 |
. . 3
⊢ (𝑣 = ∅ → (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐹‘𝑣) ≠ 𝑥) ↔ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘∅) ≠ 𝑥))) |
4 | | fveq2 6717 |
. . . . 5
⊢ (𝑣 = 𝑢 → (𝐹‘𝑣) = (𝐹‘𝑢)) |
5 | 4 | neeq1d 3000 |
. . . 4
⊢ (𝑣 = 𝑢 → ((𝐹‘𝑣) ≠ 𝑥 ↔ (𝐹‘𝑢) ≠ 𝑥)) |
6 | 5 | imbi2d 344 |
. . 3
⊢ (𝑣 = 𝑢 → (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘𝑣) ≠ 𝑥) ↔ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘𝑢) ≠ 𝑥))) |
7 | | fveq2 6717 |
. . . . 5
⊢ (𝑣 = suc 𝑢 → (𝐹‘𝑣) = (𝐹‘suc 𝑢)) |
8 | 7 | neeq1d 3000 |
. . . 4
⊢ (𝑣 = suc 𝑢 → ((𝐹‘𝑣) ≠ 𝑥 ↔ (𝐹‘suc 𝑢) ≠ 𝑥)) |
9 | 8 | imbi2d 344 |
. . 3
⊢ (𝑣 = suc 𝑢 → (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘𝑣) ≠ 𝑥) ↔ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘suc 𝑢) ≠ 𝑥))) |
10 | | fveq2 6717 |
. . . . 5
⊢ (𝑣 = 𝐴 → (𝐹‘𝑣) = (𝐹‘𝐴)) |
11 | 10 | neeq1d 3000 |
. . . 4
⊢ (𝑣 = 𝐴 → ((𝐹‘𝑣) ≠ 𝑥 ↔ (𝐹‘𝐴) ≠ 𝑥)) |
12 | 11 | imbi2d 344 |
. . 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 9240 |
. . . . . . 7
⊢ (𝐹‘∅) =
∅ |
18 | 17 | eqeq1i 2742 |
. . . . . 6
⊢ ((𝐹‘∅) = 𝑥 ↔ ∅ = 𝑥) |
19 | | eqcom 2744 |
. . . . . 6
⊢ (∅
= 𝑥 ↔ 𝑥 = ∅) |
20 | 18, 19 | sylbb 222 |
. . . . 5
⊢ ((𝐹‘∅) = 𝑥 → 𝑥 = ∅) |
21 | 20 | necon3i 2973 |
. . . 4
⊢ (𝑥 ≠ ∅ → (𝐹‘∅) ≠ 𝑥) |
22 | 21 | adantr 484 |
. . 3
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐹‘∅)
≠ 𝑥) |
23 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑢 ∈ V |
24 | 13, 14, 23, 16 | inf3lemd 9242 |
. . . . . . . 8
⊢ (𝑢 ∈ ω → (𝐹‘𝑢) ⊆ 𝑥) |
25 | | df-pss 3885 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑢) ⊊ 𝑥 ↔ ((𝐹‘𝑢) ⊆ 𝑥 ∧ (𝐹‘𝑢) ≠ 𝑥)) |
26 | | pssnel 4385 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑢) ⊊ 𝑥 → ∃𝑣(𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ (𝐹‘𝑢))) |
27 | 25, 26 | sylbir 238 |
. . . . . . . . 9
⊢ (((𝐹‘𝑢) ⊆ 𝑥 ∧ (𝐹‘𝑢) ≠ 𝑥) → ∃𝑣(𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ (𝐹‘𝑢))) |
28 | | ssel 3893 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ ∪ 𝑥
→ (𝑣 ∈ 𝑥 → 𝑣 ∈ ∪ 𝑥)) |
29 | | eluni 4822 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ ∪ 𝑥
↔ ∃𝑓(𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥)) |
30 | 28, 29 | syl6ib 254 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ∪ 𝑥
→ (𝑣 ∈ 𝑥 → ∃𝑓(𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥))) |
31 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘suc 𝑢) = 𝑥 → (𝑓 ∈ (𝐹‘suc 𝑢) ↔ 𝑓 ∈ 𝑥)) |
32 | 31 | biimparc 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ 𝑥 ∧ (𝐹‘suc 𝑢) = 𝑥) → 𝑓 ∈ (𝐹‘suc 𝑢)) |
33 | 13, 14, 23, 16 | inf3lemc 9241 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ ω → (𝐹‘suc 𝑢) = (𝐺‘(𝐹‘𝑢))) |
34 | 33 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ ω → (𝑓 ∈ (𝐹‘suc 𝑢) ↔ 𝑓 ∈ (𝐺‘(𝐹‘𝑢)))) |
35 | | elin 3882 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ (𝑓 ∩ 𝑥) ↔ (𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥)) |
36 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑓 ∈ V |
37 | | fvex 6730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹‘𝑢) ∈ V |
38 | 13, 14, 36, 37 | inf3lema 9239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 ∈ (𝐺‘(𝐹‘𝑢)) ↔ (𝑓 ∈ 𝑥 ∧ (𝑓 ∩ 𝑥) ⊆ (𝐹‘𝑢))) |
39 | 38 | simprbi 500 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ (𝐺‘(𝐹‘𝑢)) → (𝑓 ∩ 𝑥) ⊆ (𝐹‘𝑢)) |
40 | 39 | sseld 3900 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ (𝐺‘(𝐹‘𝑢)) → (𝑣 ∈ (𝑓 ∩ 𝑥) → 𝑣 ∈ (𝐹‘𝑢))) |
41 | 35, 40 | syl5bir 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ (𝐺‘(𝐹‘𝑢)) → ((𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ (𝐹‘𝑢))) |
42 | 34, 41 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ω → (𝑓 ∈ (𝐹‘suc 𝑢) → ((𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ (𝐹‘𝑢)))) |
43 | 32, 42 | syl5 34 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ω → ((𝑓 ∈ 𝑥 ∧ (𝐹‘suc 𝑢) = 𝑥) → ((𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ (𝐹‘𝑢)))) |
44 | 43 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ω → ((𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥) → ((𝑓 ∈ 𝑥 ∧ (𝐹‘suc 𝑢) = 𝑥) → 𝑣 ∈ (𝐹‘𝑢)))) |
45 | 44 | exp5c 448 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ω → (𝑣 ∈ 𝑓 → (𝑣 ∈ 𝑥 → (𝑓 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢)))))) |
46 | 45 | com34 91 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ω → (𝑣 ∈ 𝑓 → (𝑓 ∈ 𝑥 → (𝑣 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢)))))) |
47 | 46 | impd 414 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ω → ((𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥) → (𝑣 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢))))) |
48 | 47 | exlimdv 1941 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ω →
(∃𝑓(𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥) → (𝑣 ∈ 𝑥 → ((𝐹‘suc 𝑢) = 𝑥 → 𝑣 ∈ (𝐹‘𝑢))))) |
49 | 30, 48 | sylan9r 512 |
. . . . . . . . . . . . 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 414 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ (𝐹‘𝑢)) → (𝐹‘suc 𝑢) ≠ 𝑥)) |
55 | 54 | exlimdv 1941 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ (∃𝑣(𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ (𝐹‘𝑢)) → (𝐹‘suc 𝑢) ≠ 𝑥)) |
56 | 27, 55 | syl5 34 |
. . . . . . . 8
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ (((𝐹‘𝑢) ⊆ 𝑥 ∧ (𝐹‘𝑢) ≠ 𝑥) → (𝐹‘suc 𝑢) ≠ 𝑥)) |
57 | 24, 56 | sylani 607 |
. . . . . . 7
⊢ ((𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝑢 ∈ ω
∧ (𝐹‘𝑢) ≠ 𝑥) → (𝐹‘suc 𝑢) ≠ 𝑥)) |
58 | 57 | exp4b 434 |
. . . . . 6
⊢ (𝑢 ∈ ω → (𝑥 ⊆ ∪ 𝑥
→ (𝑢 ∈ ω
→ ((𝐹‘𝑢) ≠ 𝑥 → (𝐹‘suc 𝑢) ≠ 𝑥)))) |
59 | 58 | pm2.43a 54 |
. . . . 5
⊢ (𝑢 ∈ ω → (𝑥 ⊆ ∪ 𝑥
→ ((𝐹‘𝑢) ≠ 𝑥 → (𝐹‘suc 𝑢) ≠ 𝑥))) |
60 | 59 | adantld 494 |
. . . 4
⊢ (𝑢 ∈ ω → ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝐹‘𝑢) ≠ 𝑥 → (𝐹‘suc 𝑢) ≠ 𝑥))) |
61 | 60 | a2d 29 |
. . 3
⊢ (𝑢 ∈ ω → (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐹‘𝑢) ≠ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘suc 𝑢) ≠ 𝑥))) |
62 | 3, 6, 9, 12, 22, 61 | finds 7676 |
. 2
⊢ (𝐴 ∈ ω → ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐹‘𝐴) ≠ 𝑥)) |
63 | 62 | com12 32 |
1
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐴 ∈ ω
→ (𝐹‘𝐴) ≠ 𝑥)) |