Proof of Theorem finxpreclem3
Step | Hyp | Ref
| Expression |
1 | | df-ov 6653 |
. 2
⊢ (𝑁𝐹𝑋) = (𝐹‘〈𝑁, 𝑋〉) |
2 | | finxpreclem3.1 |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
3 | 2 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑋 ∈ (V × 𝑈)) → 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))) |
4 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑛 = 1𝑜 ↔ 𝑁 =
1𝑜)) |
5 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) |
6 | 4, 5 | bi2anan9 917 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → ((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈) ↔ (𝑁 = 1𝑜 ∧ 𝑋 ∈ 𝑈))) |
7 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 ∈ (V × 𝑈) ↔ 𝑋 ∈ (V × 𝑈))) |
8 | 7 | adantl 482 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → (𝑥 ∈ (V × 𝑈) ↔ 𝑋 ∈ (V × 𝑈))) |
9 | | unieq 4444 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ∪ 𝑛 = ∪
𝑁) |
10 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → ∪ 𝑛 = ∪
𝑁) |
11 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (1st ‘𝑥) = (1st ‘𝑋)) |
12 | 11 | adantl 482 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → (1st ‘𝑥) = (1st ‘𝑋)) |
13 | 10, 12 | opeq12d 4410 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → 〈∪
𝑛, (1st
‘𝑥)〉 =
〈∪ 𝑁, (1st ‘𝑋)〉) |
14 | | opeq12 4404 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → 〈𝑛, 𝑥〉 = 〈𝑁, 𝑋〉) |
15 | 8, 13, 14 | ifbieq12d 4113 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) |
16 | 6, 15 | ifbieq2d 4111 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if((𝑁 = 1𝑜 ∧ 𝑋 ∈ 𝑈), ∅, if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉))) |
17 | | sssucid 5802 |
. . . . . . . . . . . . 13
⊢
1𝑜 ⊆ suc 1𝑜 |
18 | | df-2o 7561 |
. . . . . . . . . . . . 13
⊢
2𝑜 = suc 1𝑜 |
19 | 17, 18 | sseqtr4i 3638 |
. . . . . . . . . . . 12
⊢
1𝑜 ⊆ 2𝑜 |
20 | | 1on 7567 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ On |
21 | 18, 20 | sucneqoni 33214 |
. . . . . . . . . . . . 13
⊢
2𝑜 ≠ 1𝑜 |
22 | 21 | necomi 2848 |
. . . . . . . . . . . 12
⊢
1𝑜 ≠ 2𝑜 |
23 | | df-pss 3590 |
. . . . . . . . . . . 12
⊢
(1𝑜 ⊊ 2𝑜 ↔
(1𝑜 ⊆ 2𝑜 ∧
1𝑜 ≠ 2𝑜)) |
24 | 19, 22, 23 | mpbir2an 955 |
. . . . . . . . . . 11
⊢
1𝑜 ⊊ 2𝑜 |
25 | | ssnpss 3710 |
. . . . . . . . . . 11
⊢
(2𝑜 ⊆ 1𝑜 → ¬
1𝑜 ⊊ 2𝑜) |
26 | 24, 25 | mt2 191 |
. . . . . . . . . 10
⊢ ¬
2𝑜 ⊆ 1𝑜 |
27 | | sseq2 3627 |
. . . . . . . . . 10
⊢ (𝑁 = 1𝑜 →
(2𝑜 ⊆ 𝑁 ↔ 2𝑜 ⊆
1𝑜)) |
28 | 26, 27 | mtbiri 317 |
. . . . . . . . 9
⊢ (𝑁 = 1𝑜 →
¬ 2𝑜 ⊆ 𝑁) |
29 | 28 | con2i 134 |
. . . . . . . 8
⊢
(2𝑜 ⊆ 𝑁 → ¬ 𝑁 = 1𝑜) |
30 | 29 | intnanrd 963 |
. . . . . . 7
⊢
(2𝑜 ⊆ 𝑁 → ¬ (𝑁 = 1𝑜 ∧ 𝑋 ∈ 𝑈)) |
31 | 30 | iffalsed 4097 |
. . . . . 6
⊢
(2𝑜 ⊆ 𝑁 → if((𝑁 = 1𝑜 ∧ 𝑋 ∈ 𝑈), ∅, if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) = if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) |
32 | | iftrue 4092 |
. . . . . 6
⊢ (𝑋 ∈ (V × 𝑈) → if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉) = 〈∪
𝑁, (1st
‘𝑋)〉) |
33 | 31, 32 | sylan9eq 2676 |
. . . . 5
⊢
((2𝑜 ⊆ 𝑁 ∧ 𝑋 ∈ (V × 𝑈)) → if((𝑁 = 1𝑜 ∧ 𝑋 ∈ 𝑈), ∅, if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) = 〈∪ 𝑁,
(1st ‘𝑋)〉) |
34 | 16, 33 | sylan9eqr 2678 |
. . . 4
⊢
(((2𝑜 ⊆ 𝑁 ∧ 𝑋 ∈ (V × 𝑈)) ∧ (𝑛 = 𝑁 ∧ 𝑥 = 𝑋)) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = 〈∪
𝑁, (1st
‘𝑋)〉) |
35 | 34 | adantlll 754 |
. . 3
⊢ ((((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑋 ∈ (V × 𝑈)) ∧ (𝑛 = 𝑁 ∧ 𝑥 = 𝑋)) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = 〈∪
𝑁, (1st
‘𝑋)〉) |
36 | | simpll 790 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑋 ∈ (V × 𝑈)) → 𝑁 ∈ ω) |
37 | | elex 3212 |
. . . 4
⊢ (𝑋 ∈ (V × 𝑈) → 𝑋 ∈ V) |
38 | 37 | adantl 482 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑋 ∈ (V × 𝑈)) → 𝑋 ∈ V) |
39 | | opex 4932 |
. . . 4
⊢
〈∪ 𝑁, (1st ‘𝑋)〉 ∈ V |
40 | 39 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑋 ∈ (V × 𝑈)) → 〈∪
𝑁, (1st
‘𝑋)〉 ∈
V) |
41 | 3, 35, 36, 38, 40 | ovmpt2d 6788 |
. 2
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑋 ∈ (V × 𝑈)) → (𝑁𝐹𝑋) = 〈∪ 𝑁, (1st ‘𝑋)〉) |
42 | 1, 41 | syl5reqr 2671 |
1
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑋 ∈ (V × 𝑈)) → 〈∪
𝑁, (1st
‘𝑋)〉 = (𝐹‘〈𝑁, 𝑋〉)) |