Proof of Theorem finxpreclem5
Step | Hyp | Ref
| Expression |
1 | | df-ov 6881 |
. . 3
⊢ (𝑛𝐹𝑥) = (𝐹‘〈𝑛, 𝑥〉) |
2 | | vex 3388 |
. . . . . 6
⊢ 𝑥 ∈ V |
3 | | 0ex 4984 |
. . . . . . 7
⊢ ∅
∈ V |
4 | | opex 5123 |
. . . . . . . 8
⊢
〈∪ 𝑛, (1st ‘𝑥)〉 ∈ V |
5 | | opex 5123 |
. . . . . . . 8
⊢
〈𝑛, 𝑥〉 ∈ V |
6 | 4, 5 | ifex 4325 |
. . . . . . 7
⊢ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) ∈ V |
7 | 3, 6 | ifex 4325 |
. . . . . 6
⊢ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V |
8 | | finxpreclem5.1 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
9 | 8 | ovmpt4g 7017 |
. . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑥 ∈ V ∧ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V) → (𝑛𝐹𝑥) = if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
10 | 2, 7, 9 | mp3an23 1578 |
. . . . 5
⊢ (𝑛 ∈ ω → (𝑛𝐹𝑥) = if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
11 | 10 | ad2antrr 718 |
. . . 4
⊢ (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (𝑛𝐹𝑥) = if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
12 | | 1on 7806 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ On |
13 | 12 | onirri 6047 |
. . . . . . . . . 10
⊢ ¬
1𝑜 ∈ 1𝑜 |
14 | | eleq2 2867 |
. . . . . . . . . 10
⊢ (𝑛 = 1𝑜 →
(1𝑜 ∈ 𝑛 ↔ 1𝑜 ∈
1𝑜)) |
15 | 13, 14 | mtbiri 319 |
. . . . . . . . 9
⊢ (𝑛 = 1𝑜 →
¬ 1𝑜 ∈ 𝑛) |
16 | 15 | con2i 137 |
. . . . . . . 8
⊢
(1𝑜 ∈ 𝑛 → ¬ 𝑛 = 1𝑜) |
17 | 16 | intnanrd 484 |
. . . . . . 7
⊢
(1𝑜 ∈ 𝑛 → ¬ (𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈)) |
18 | 17 | iffalsed 4288 |
. . . . . 6
⊢
(1𝑜 ∈ 𝑛 → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) |
19 | 18 | adantl 474 |
. . . . 5
⊢ ((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) |
20 | | iffalse 4286 |
. . . . 5
⊢ (¬
𝑥 ∈ (V × 𝑈) → if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) |
21 | 19, 20 | sylan9eq 2853 |
. . . 4
⊢ (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = 〈𝑛, 𝑥〉) |
22 | 11, 21 | eqtrd 2833 |
. . 3
⊢ (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (𝑛𝐹𝑥) = 〈𝑛, 𝑥〉) |
23 | 1, 22 | syl5eqr 2847 |
. 2
⊢ (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (𝐹‘〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) |
24 | 23 | ex 402 |
1
⊢ ((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) → (¬ 𝑥 ∈ (V × 𝑈) → (𝐹‘〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉)) |