| Step | Hyp | Ref
| Expression |
| 1 | | inf3lem.1 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) |
| 2 | | inf3lem.2 |
. . . . . . . . . . 11
⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) |
| 3 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑢 ∈ V |
| 4 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑣 ∈ V |
| 5 | 1, 2, 3, 4 | inf3lem5 9672 |
. . . . . . . . . 10
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝑢 ∈ ω
∧ 𝑣 ∈ 𝑢) → (𝐹‘𝑣) ⊊ (𝐹‘𝑢))) |
| 6 | | dfpss2 4088 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑣) ⊊ (𝐹‘𝑢) ↔ ((𝐹‘𝑣) ⊆ (𝐹‘𝑢) ∧ ¬ (𝐹‘𝑣) = (𝐹‘𝑢))) |
| 7 | 6 | simprbi 496 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑣) ⊊ (𝐹‘𝑢) → ¬ (𝐹‘𝑣) = (𝐹‘𝑢)) |
| 8 | 5, 7 | syl6 35 |
. . . . . . . . 9
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝑢 ∈ ω
∧ 𝑣 ∈ 𝑢) → ¬ (𝐹‘𝑣) = (𝐹‘𝑢))) |
| 9 | 8 | expdimp 452 |
. . . . . . . 8
⊢ (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
∧ 𝑢 ∈ ω)
→ (𝑣 ∈ 𝑢 → ¬ (𝐹‘𝑣) = (𝐹‘𝑢))) |
| 10 | 9 | adantrl 716 |
. . . . . . 7
⊢ (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
∧ (𝑣 ∈ ω
∧ 𝑢 ∈ ω))
→ (𝑣 ∈ 𝑢 → ¬ (𝐹‘𝑣) = (𝐹‘𝑢))) |
| 11 | 1, 2, 4, 3 | inf3lem5 9672 |
. . . . . . . . . 10
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝑣 ∈ ω
∧ 𝑢 ∈ 𝑣) → (𝐹‘𝑢) ⊊ (𝐹‘𝑣))) |
| 12 | | dfpss2 4088 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑢) ⊊ (𝐹‘𝑣) ↔ ((𝐹‘𝑢) ⊆ (𝐹‘𝑣) ∧ ¬ (𝐹‘𝑢) = (𝐹‘𝑣))) |
| 13 | 12 | simprbi 496 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑢) ⊊ (𝐹‘𝑣) → ¬ (𝐹‘𝑢) = (𝐹‘𝑣)) |
| 14 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑢) = (𝐹‘𝑣) ↔ (𝐹‘𝑣) = (𝐹‘𝑢)) |
| 15 | 13, 14 | sylnib 328 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑢) ⊊ (𝐹‘𝑣) → ¬ (𝐹‘𝑣) = (𝐹‘𝑢)) |
| 16 | 11, 15 | syl6 35 |
. . . . . . . . 9
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ ((𝑣 ∈ ω
∧ 𝑢 ∈ 𝑣) → ¬ (𝐹‘𝑣) = (𝐹‘𝑢))) |
| 17 | 16 | expdimp 452 |
. . . . . . . 8
⊢ (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
∧ 𝑣 ∈ ω)
→ (𝑢 ∈ 𝑣 → ¬ (𝐹‘𝑣) = (𝐹‘𝑢))) |
| 18 | 17 | adantrr 717 |
. . . . . . 7
⊢ (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
∧ (𝑣 ∈ ω
∧ 𝑢 ∈ ω))
→ (𝑢 ∈ 𝑣 → ¬ (𝐹‘𝑣) = (𝐹‘𝑢))) |
| 19 | 10, 18 | jaod 860 |
. . . . . 6
⊢ (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
∧ (𝑣 ∈ ω
∧ 𝑢 ∈ ω))
→ ((𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣) → ¬ (𝐹‘𝑣) = (𝐹‘𝑢))) |
| 20 | 19 | con2d 134 |
. . . . 5
⊢ (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
∧ (𝑣 ∈ ω
∧ 𝑢 ∈ ω))
→ ((𝐹‘𝑣) = (𝐹‘𝑢) → ¬ (𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣))) |
| 21 | | nnord 7895 |
. . . . . . 7
⊢ (𝑣 ∈ ω → Ord 𝑣) |
| 22 | | nnord 7895 |
. . . . . . 7
⊢ (𝑢 ∈ ω → Ord 𝑢) |
| 23 | | ordtri3 6420 |
. . . . . . 7
⊢ ((Ord
𝑣 ∧ Ord 𝑢) → (𝑣 = 𝑢 ↔ ¬ (𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣))) |
| 24 | 21, 22, 23 | syl2an 596 |
. . . . . 6
⊢ ((𝑣 ∈ ω ∧ 𝑢 ∈ ω) → (𝑣 = 𝑢 ↔ ¬ (𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣))) |
| 25 | 24 | adantl 481 |
. . . . 5
⊢ (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
∧ (𝑣 ∈ ω
∧ 𝑢 ∈ ω))
→ (𝑣 = 𝑢 ↔ ¬ (𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣))) |
| 26 | 20, 25 | sylibrd 259 |
. . . 4
⊢ (((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
∧ (𝑣 ∈ ω
∧ 𝑢 ∈ ω))
→ ((𝐹‘𝑣) = (𝐹‘𝑢) → 𝑣 = 𝑢)) |
| 27 | 26 | ralrimivva 3202 |
. . 3
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ ∀𝑣 ∈
ω ∀𝑢 ∈
ω ((𝐹‘𝑣) = (𝐹‘𝑢) → 𝑣 = 𝑢)) |
| 28 | | frfnom 8475 |
. . . . . 6
⊢
(rec(𝐺, ∅)
↾ ω) Fn ω |
| 29 | | fneq1 6659 |
. . . . . 6
⊢ (𝐹 = (rec(𝐺, ∅) ↾ ω) → (𝐹 Fn ω ↔ (rec(𝐺, ∅) ↾ ω) Fn
ω)) |
| 30 | 28, 29 | mpbiri 258 |
. . . . 5
⊢ (𝐹 = (rec(𝐺, ∅) ↾ ω) → 𝐹 Fn ω) |
| 31 | | fvelrnb 6969 |
. . . . . . . 8
⊢ (𝐹 Fn ω → (𝑢 ∈ ran 𝐹 ↔ ∃𝑣 ∈ ω (𝐹‘𝑣) = 𝑢)) |
| 32 | | inf3lem.4 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
| 33 | 1, 2, 4, 32 | inf3lemd 9667 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ω → (𝐹‘𝑣) ⊆ 𝑥) |
| 34 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑣) ∈ V |
| 35 | 34 | elpw 4604 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑣) ∈ 𝒫 𝑥 ↔ (𝐹‘𝑣) ⊆ 𝑥) |
| 36 | 33, 35 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ω → (𝐹‘𝑣) ∈ 𝒫 𝑥) |
| 37 | | eleq1 2829 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑣) = 𝑢 → ((𝐹‘𝑣) ∈ 𝒫 𝑥 ↔ 𝑢 ∈ 𝒫 𝑥)) |
| 38 | 36, 37 | syl5ibcom 245 |
. . . . . . . . 9
⊢ (𝑣 ∈ ω → ((𝐹‘𝑣) = 𝑢 → 𝑢 ∈ 𝒫 𝑥)) |
| 39 | 38 | rexlimiv 3148 |
. . . . . . . 8
⊢
(∃𝑣 ∈
ω (𝐹‘𝑣) = 𝑢 → 𝑢 ∈ 𝒫 𝑥) |
| 40 | 31, 39 | biimtrdi 253 |
. . . . . . 7
⊢ (𝐹 Fn ω → (𝑢 ∈ ran 𝐹 → 𝑢 ∈ 𝒫 𝑥)) |
| 41 | 40 | ssrdv 3989 |
. . . . . 6
⊢ (𝐹 Fn ω → ran 𝐹 ⊆ 𝒫 𝑥) |
| 42 | 41 | ancli 548 |
. . . . 5
⊢ (𝐹 Fn ω → (𝐹 Fn ω ∧ ran 𝐹 ⊆ 𝒫 𝑥)) |
| 43 | 2, 30, 42 | mp2b 10 |
. . . 4
⊢ (𝐹 Fn ω ∧ ran 𝐹 ⊆ 𝒫 𝑥) |
| 44 | | df-f 6565 |
. . . 4
⊢ (𝐹:ω⟶𝒫 𝑥 ↔ (𝐹 Fn ω ∧ ran 𝐹 ⊆ 𝒫 𝑥)) |
| 45 | 43, 44 | mpbir 231 |
. . 3
⊢ 𝐹:ω⟶𝒫 𝑥 |
| 46 | 27, 45 | jctil 519 |
. 2
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ (𝐹:ω⟶𝒫 𝑥 ∧ ∀𝑣 ∈ ω ∀𝑢 ∈ ω ((𝐹‘𝑣) = (𝐹‘𝑢) → 𝑣 = 𝑢))) |
| 47 | | dff13 7275 |
. 2
⊢ (𝐹:ω–1-1→𝒫 𝑥 ↔ (𝐹:ω⟶𝒫 𝑥 ∧ ∀𝑣 ∈ ω ∀𝑢 ∈ ω ((𝐹‘𝑣) = (𝐹‘𝑢) → 𝑣 = 𝑢))) |
| 48 | 46, 47 | sylibr 234 |
1
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
→ 𝐹:ω–1-1→𝒫 𝑥) |