Proof of Theorem finxpreclem5
Step | Hyp | Ref
| Expression |
1 | | df-ov 7280 |
. . 3
⊢ (𝑛𝐹𝑥) = (𝐹‘〈𝑛, 𝑥〉) |
2 | | vex 3435 |
. . . . . 6
⊢ 𝑥 ∈ V |
3 | | 0ex 5233 |
. . . . . . 7
⊢ ∅
∈ V |
4 | | opex 5381 |
. . . . . . . 8
⊢
〈∪ 𝑛, (1st ‘𝑥)〉 ∈ V |
5 | | opex 5381 |
. . . . . . . 8
⊢
〈𝑛, 𝑥〉 ∈ V |
6 | 4, 5 | ifex 4511 |
. . . . . . 7
⊢ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) ∈ V |
7 | 3, 6 | ifex 4511 |
. . . . . 6
⊢ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V |
8 | | finxpreclem5.1 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
9 | 8 | ovmpt4g 7420 |
. . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑥 ∈ V ∧ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V) → (𝑛𝐹𝑥) = if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
10 | 2, 7, 9 | mp3an23 1452 |
. . . . 5
⊢ (𝑛 ∈ ω → (𝑛𝐹𝑥) = if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
11 | 10 | ad2antrr 723 |
. . . 4
⊢ (((𝑛 ∈ ω ∧
1o ∈ 𝑛)
∧ ¬ 𝑥 ∈ (V
× 𝑈)) → (𝑛𝐹𝑥) = if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
12 | | 1on 8307 |
. . . . . . . . . . 11
⊢
1o ∈ On |
13 | 12 | onirri 6375 |
. . . . . . . . . 10
⊢ ¬
1o ∈ 1o |
14 | | eleq2 2827 |
. . . . . . . . . 10
⊢ (𝑛 = 1o →
(1o ∈ 𝑛
↔ 1o ∈ 1o)) |
15 | 13, 14 | mtbiri 327 |
. . . . . . . . 9
⊢ (𝑛 = 1o → ¬
1o ∈ 𝑛) |
16 | 15 | con2i 139 |
. . . . . . . 8
⊢
(1o ∈ 𝑛 → ¬ 𝑛 = 1o) |
17 | 16 | intnanrd 490 |
. . . . . . 7
⊢
(1o ∈ 𝑛 → ¬ (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)) |
18 | 17 | iffalsed 4472 |
. . . . . 6
⊢
(1o ∈ 𝑛 → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) |
19 | 18 | adantl 482 |
. . . . 5
⊢ ((𝑛 ∈ ω ∧
1o ∈ 𝑛)
→ if((𝑛 =
1o ∧ 𝑥
∈ 𝑈), ∅,
if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) |
20 | | iffalse 4470 |
. . . . 5
⊢ (¬
𝑥 ∈ (V × 𝑈) → if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) |
21 | 19, 20 | sylan9eq 2798 |
. . . 4
⊢ (((𝑛 ∈ ω ∧
1o ∈ 𝑛)
∧ ¬ 𝑥 ∈ (V
× 𝑈)) →
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = 〈𝑛, 𝑥〉) |
22 | 11, 21 | eqtrd 2778 |
. . 3
⊢ (((𝑛 ∈ ω ∧
1o ∈ 𝑛)
∧ ¬ 𝑥 ∈ (V
× 𝑈)) → (𝑛𝐹𝑥) = 〈𝑛, 𝑥〉) |
23 | 1, 22 | eqtr3id 2792 |
. 2
⊢ (((𝑛 ∈ ω ∧
1o ∈ 𝑛)
∧ ¬ 𝑥 ∈ (V
× 𝑈)) → (𝐹‘〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) |
24 | 23 | ex 413 |
1
⊢ ((𝑛 ∈ ω ∧
1o ∈ 𝑛)
→ (¬ 𝑥 ∈ (V
× 𝑈) → (𝐹‘〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉)) |