Proof of Theorem pwfseqlem4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ 𝑍 = 𝑍 | 
| 2 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ (𝑊‘𝑍) = (𝑊‘𝑍) | 
| 3 | 1, 2 | pm3.2i 470 | . . . . . . . . . . . 12
⊢ (𝑍 = 𝑍 ∧ (𝑊‘𝑍) = (𝑊‘𝑍)) | 
| 4 |  | pwfseqlem4.w | . . . . . . . . . . . . 13
⊢ 𝑊 = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))} | 
| 5 |  | pwfseqlem4.g | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) | 
| 6 |  | omex 9683 | . . . . . . . . . . . . . . . 16
⊢ ω
∈ V | 
| 7 |  | ovex 7464 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ↑m 𝑛) ∈ V | 
| 8 | 6, 7 | iunex 7993 | . . . . . . . . . . . . . . 15
⊢ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∈ V | 
| 9 |  | f1dmex 7981 | . . . . . . . . . . . . . . 15
⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V) | 
| 10 | 5, 8, 9 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝒫 𝐴 ∈ V) | 
| 11 |  | pwexb 7786 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) | 
| 12 | 10, 11 | sylibr 234 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ V) | 
| 13 |  | pwfseqlem4.x | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ⊆ 𝐴) | 
| 14 |  | pwfseqlem4.h | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) | 
| 15 |  | pwfseqlem4.ps | . . . . . . . . . . . . . 14
⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) | 
| 16 |  | pwfseqlem4.k | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥) | 
| 17 |  | pwfseqlem4.d | . . . . . . . . . . . . . 14
⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) | 
| 18 |  | pwfseqlem4.f | . . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) | 
| 19 | 5, 13, 14, 15, 16, 17, 18 | pwfseqlem4a 10701 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴) | 
| 20 |  | pwfseqlem4.z | . . . . . . . . . . . . 13
⊢ 𝑍 = ∪
dom 𝑊 | 
| 21 | 4, 12, 19, 20 | fpwwe2 10683 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑍𝑊(𝑊‘𝑍) ∧ (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍) ↔ (𝑍 = 𝑍 ∧ (𝑊‘𝑍) = (𝑊‘𝑍)))) | 
| 22 | 3, 21 | mpbiri 258 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑍𝑊(𝑊‘𝑍) ∧ (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍)) | 
| 23 | 22 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 𝑍𝑊(𝑊‘𝑍)) | 
| 24 | 4, 12 | fpwwe2lem2 10672 | . . . . . . . . . 10
⊢ (𝜑 → (𝑍𝑊(𝑊‘𝑍) ↔ ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏)))) | 
| 25 | 23, 24 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏))) | 
| 26 |  | id 22 | . . . . . . . . . . 11
⊢ ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍) → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍)) | 
| 27 | 26 | 3expa 1119 | . . . . . . . . . 10
⊢ (((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ (𝑊‘𝑍) We 𝑍) → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍)) | 
| 28 | 27 | adantrr 717 | . . . . . . . . 9
⊢ (((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏)) → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍)) | 
| 29 | 25, 28 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍)) | 
| 30 | 22 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍) | 
| 31 | 25 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍))) | 
| 32 | 31 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 𝑍 ⊆ 𝐴) | 
| 33 | 12, 32 | ssexd 5324 | . . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ V) | 
| 34 |  | fvexd 6921 | . . . . . . . . 9
⊢ (𝜑 → (𝑊‘𝑍) ∈ V) | 
| 35 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → 𝑎 = 𝑍) | 
| 36 | 35 | sseq1d 4015 | . . . . . . . . . . 11
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑎 ⊆ 𝐴 ↔ 𝑍 ⊆ 𝐴)) | 
| 37 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → 𝑠 = (𝑊‘𝑍)) | 
| 38 | 35 | sqxpeqd 5717 | . . . . . . . . . . . 12
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑎 × 𝑎) = (𝑍 × 𝑍)) | 
| 39 | 37, 38 | sseq12d 4017 | . . . . . . . . . . 11
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑠 ⊆ (𝑎 × 𝑎) ↔ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍))) | 
| 40 | 37, 35 | weeq12d 5674 | . . . . . . . . . . 11
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑠 We 𝑎 ↔ (𝑊‘𝑍) We 𝑍)) | 
| 41 | 36, 39, 40 | 3anbi123d 1438 | . . . . . . . . . 10
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ↔ (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))) | 
| 42 |  | oveq12 7440 | . . . . . . . . . . . 12
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑎𝐹𝑠) = (𝑍𝐹(𝑊‘𝑍))) | 
| 43 | 42, 35 | eleq12d 2835 | . . . . . . . . . . 11
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → ((𝑎𝐹𝑠) ∈ 𝑎 ↔ (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍)) | 
| 44 | 35 | breq1d 5153 | . . . . . . . . . . 11
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑎 ≺ ω ↔ 𝑍 ≺ ω)) | 
| 45 | 43, 44 | imbi12d 344 | . . . . . . . . . 10
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω) ↔ ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω))) | 
| 46 | 41, 45 | imbi12d 344 | . . . . . . . . 9
⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) → ((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω)) ↔ ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍) → ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω)))) | 
| 47 |  | omelon 9686 | . . . . . . . . . . . . . 14
⊢ ω
∈ On | 
| 48 |  | onenon 9989 | . . . . . . . . . . . . . 14
⊢ (ω
∈ On → ω ∈ dom card) | 
| 49 | 47, 48 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ ω
∈ dom card | 
| 50 |  | simpr3 1197 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑠 We 𝑎) | 
| 51 | 50 | 19.8ad 2182 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ∃𝑠 𝑠 We 𝑎) | 
| 52 |  | ween 10075 | . . . . . . . . . . . . . 14
⊢ (𝑎 ∈ dom card ↔
∃𝑠 𝑠 We 𝑎) | 
| 53 | 51, 52 | sylibr 234 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑎 ∈ dom card) | 
| 54 |  | domtri2 10029 | . . . . . . . . . . . . 13
⊢ ((ω
∈ dom card ∧ 𝑎
∈ dom card) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω)) | 
| 55 | 49, 53, 54 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω)) | 
| 56 |  | nfv 1914 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑟(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) | 
| 57 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑟𝑎 | 
| 58 |  | nfmpo2 7514 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) | 
| 59 | 18, 58 | nfcxfr 2903 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑟𝐹 | 
| 60 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑟𝑠 | 
| 61 | 57, 59, 60 | nfov 7461 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑟(𝑎𝐹𝑠) | 
| 62 | 61 | nfel1 2922 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑟(𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎) | 
| 63 | 56, 62 | nfim 1896 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑟((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)) | 
| 64 |  | sseq1 4009 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = 𝑠 → (𝑟 ⊆ (𝑎 × 𝑎) ↔ 𝑠 ⊆ (𝑎 × 𝑎))) | 
| 65 |  | weeq1 5672 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = 𝑠 → (𝑟 We 𝑎 ↔ 𝑠 We 𝑎)) | 
| 66 | 64, 65 | 3anbi23d 1441 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑠 → ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎))) | 
| 67 | 66 | anbi1d 631 | . . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑠 → (((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎))) | 
| 68 | 67 | anbi2d 630 | . . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑠 → ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)))) | 
| 69 |  | oveq2 7439 | . . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑠 → (𝑎𝐹𝑟) = (𝑎𝐹𝑠)) | 
| 70 | 69 | eleq1d 2826 | . . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑠 → ((𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎) ↔ (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎))) | 
| 71 | 68, 70 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑠 → (((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)))) | 
| 72 |  | nfv 1914 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) | 
| 73 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝑎 | 
| 74 |  | nfmpo1 7513 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) | 
| 75 | 18, 74 | nfcxfr 2903 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝐹 | 
| 76 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝑟 | 
| 77 | 73, 75, 76 | nfov 7461 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝑎𝐹𝑟) | 
| 78 | 77 | nfel1 2922 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎) | 
| 79 | 72, 78 | nfim 1896 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) | 
| 80 |  | sseq1 4009 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑎 → (𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴)) | 
| 81 |  | xpeq12 5710 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 = 𝑎 ∧ 𝑥 = 𝑎) → (𝑥 × 𝑥) = (𝑎 × 𝑎)) | 
| 82 | 81 | anidms 566 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑎 → (𝑥 × 𝑥) = (𝑎 × 𝑎)) | 
| 83 | 82 | sseq2d 4016 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑎 → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑟 ⊆ (𝑎 × 𝑎))) | 
| 84 |  | weeq2 5673 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑎 → (𝑟 We 𝑥 ↔ 𝑟 We 𝑎)) | 
| 85 | 80, 83, 84 | 3anbi123d 1438 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑎 → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎))) | 
| 86 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑎 → (ω ≼ 𝑥 ↔ ω ≼ 𝑎)) | 
| 87 | 85, 86 | anbi12d 632 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))) | 
| 88 | 15, 87 | bitrid 283 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → (𝜓 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))) | 
| 89 | 88 | anbi2d 630 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)))) | 
| 90 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → (𝑥𝐹𝑟) = (𝑎𝐹𝑟)) | 
| 91 |  | difeq2 4120 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑎)) | 
| 92 | 90, 91 | eleq12d 2835 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → ((𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥) ↔ (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎))) | 
| 93 | 89, 92 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)))) | 
| 94 | 5, 13, 14, 15, 16, 17, 18 | pwfseqlem3 10700 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) | 
| 95 | 79, 93, 94 | chvarfv 2240 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) | 
| 96 | 63, 71, 95 | chvarfv 2240 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)) | 
| 97 | 96 | eldifbd 3964 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → ¬ (𝑎𝐹𝑠) ∈ 𝑎) | 
| 98 | 97 | expr 456 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 → ¬ (𝑎𝐹𝑠) ∈ 𝑎)) | 
| 99 | 55, 98 | sylbird 260 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (¬ 𝑎 ≺ ω → ¬ (𝑎𝐹𝑠) ∈ 𝑎)) | 
| 100 | 99 | con4d 115 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω)) | 
| 101 | 100 | ex 412 | . . . . . . . . 9
⊢ (𝜑 → ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) → ((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω))) | 
| 102 | 33, 34, 46, 101 | vtocl2d 3562 | . . . . . . . 8
⊢ (𝜑 → ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍) → ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω))) | 
| 103 | 29, 30, 102 | mp2d 49 | . . . . . . 7
⊢ (𝜑 → 𝑍 ≺ ω) | 
| 104 |  | isfinite 9692 | . . . . . . 7
⊢ (𝑍 ∈ Fin ↔ 𝑍 ≺
ω) | 
| 105 | 103, 104 | sylibr 234 | . . . . . 6
⊢ (𝜑 → 𝑍 ∈ Fin) | 
| 106 |  | fvex 6919 | . . . . . 6
⊢ (𝑊‘𝑍) ∈ V | 
| 107 | 5, 13, 14, 15, 16, 17, 18 | pwfseqlem2 10699 | . . . . . 6
⊢ ((𝑍 ∈ Fin ∧ (𝑊‘𝑍) ∈ V) → (𝑍𝐹(𝑊‘𝑍)) = (𝐻‘(card‘𝑍))) | 
| 108 | 105, 106,
107 | sylancl 586 | . . . . 5
⊢ (𝜑 → (𝑍𝐹(𝑊‘𝑍)) = (𝐻‘(card‘𝑍))) | 
| 109 | 108, 30 | eqeltrrd 2842 | . . . 4
⊢ (𝜑 → (𝐻‘(card‘𝑍)) ∈ 𝑍) | 
| 110 | 4, 12, 23 | fpwwe2lem3 10673 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐻‘(card‘𝑍)) ∈ 𝑍) → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘𝑍))) | 
| 111 | 109, 110 | mpdan 687 | . . . . . . . . 9
⊢ (𝜑 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘𝑍))) | 
| 112 |  | cnvimass 6100 | . . . . . . . . . . . 12
⊢ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ dom (𝑊‘𝑍) | 
| 113 | 31 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) | 
| 114 |  | dmss 5913 | . . . . . . . . . . . . . 14
⊢ ((𝑊‘𝑍) ⊆ (𝑍 × 𝑍) → dom (𝑊‘𝑍) ⊆ dom (𝑍 × 𝑍)) | 
| 115 | 113, 114 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝑊‘𝑍) ⊆ dom (𝑍 × 𝑍)) | 
| 116 |  | dmxpss 6191 | . . . . . . . . . . . . 13
⊢ dom
(𝑍 × 𝑍) ⊆ 𝑍 | 
| 117 | 115, 116 | sstrdi 3996 | . . . . . . . . . . . 12
⊢ (𝜑 → dom (𝑊‘𝑍) ⊆ 𝑍) | 
| 118 | 112, 117 | sstrid 3995 | . . . . . . . . . . 11
⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍) | 
| 119 | 105, 118 | ssfid 9301 | . . . . . . . . . 10
⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin) | 
| 120 | 106 | inex1 5317 | . . . . . . . . . 10
⊢ ((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ∈ V | 
| 121 | 5, 13, 14, 15, 16, 17, 18 | pwfseqlem2 10699 | . . . . . . . . . 10
⊢ (((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin ∧ ((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ∈ V) → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) | 
| 122 | 119, 120,
121 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) | 
| 123 | 111, 122 | eqtr3d 2779 | . . . . . . . 8
⊢ (𝜑 → (𝐻‘(card‘𝑍)) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) | 
| 124 |  | f1of1 6847 | . . . . . . . . . 10
⊢ (𝐻:ω–1-1-onto→𝑋 → 𝐻:ω–1-1→𝑋) | 
| 125 | 14, 124 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐻:ω–1-1→𝑋) | 
| 126 |  | ficardom 10001 | . . . . . . . . . 10
⊢ (𝑍 ∈ Fin →
(card‘𝑍) ∈
ω) | 
| 127 | 105, 126 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (card‘𝑍) ∈
ω) | 
| 128 |  | ficardom 10001 | . . . . . . . . . 10
⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin → (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω) | 
| 129 | 119, 128 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω) | 
| 130 |  | f1fveq 7282 | . . . . . . . . 9
⊢ ((𝐻:ω–1-1→𝑋 ∧ ((card‘𝑍) ∈ ω ∧ (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)) → ((𝐻‘(card‘𝑍)) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ↔ (card‘𝑍) = (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) | 
| 131 | 125, 127,
129, 130 | syl12anc 837 | . . . . . . . 8
⊢ (𝜑 → ((𝐻‘(card‘𝑍)) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ↔ (card‘𝑍) = (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) | 
| 132 | 123, 131 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (card‘𝑍) = (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) | 
| 133 | 132 | eqcomd 2743 | . . . . . 6
⊢ (𝜑 → (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍)) | 
| 134 |  | finnum 9988 | . . . . . . . 8
⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card) | 
| 135 | 119, 134 | syl 17 | . . . . . . 7
⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card) | 
| 136 |  | finnum 9988 | . . . . . . . 8
⊢ (𝑍 ∈ Fin → 𝑍 ∈ dom
card) | 
| 137 | 105, 136 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑍 ∈ dom card) | 
| 138 |  | carden2 10027 | . . . . . . 7
⊢ (((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card ∧ 𝑍 ∈ dom card) → ((card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍) ↔ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)) | 
| 139 | 135, 137,
138 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ((card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍) ↔ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)) | 
| 140 | 133, 139 | mpbid 232 | . . . . 5
⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍) | 
| 141 |  | dfpss2 4088 | . . . . . . . 8
⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍 ∧ ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍)) | 
| 142 | 141 | baib 535 | . . . . . . 7
⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍)) | 
| 143 | 118, 142 | syl 17 | . . . . . 6
⊢ (𝜑 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍)) | 
| 144 |  | php3 9249 | . . . . . . . . 9
⊢ ((𝑍 ∈ Fin ∧ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍) → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≺ 𝑍) | 
| 145 |  | sdomnen 9021 | . . . . . . . . 9
⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≺ 𝑍 → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍) | 
| 146 | 144, 145 | syl 17 | . . . . . . . 8
⊢ ((𝑍 ∈ Fin ∧ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍) → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍) | 
| 147 | 146 | ex 412 | . . . . . . 7
⊢ (𝑍 ∈ Fin → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)) | 
| 148 | 105, 147 | syl 17 | . . . . . 6
⊢ (𝜑 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)) | 
| 149 | 143, 148 | sylbird 260 | . . . . 5
⊢ (𝜑 → (¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍 → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)) | 
| 150 | 140, 149 | mt4d 117 | . . . 4
⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍) | 
| 151 | 109, 150 | eleqtrrd 2844 | . . 3
⊢ (𝜑 → (𝐻‘(card‘𝑍)) ∈ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) | 
| 152 |  | fvex 6919 | . . . 4
⊢ (𝐻‘(card‘𝑍)) ∈ V | 
| 153 | 152 | eliniseg 6112 | . . . 4
⊢ ((𝐻‘(card‘𝑍)) ∈ V → ((𝐻‘(card‘𝑍)) ∈ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ↔ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍)))) | 
| 154 | 152, 153 | ax-mp 5 | . . 3
⊢ ((𝐻‘(card‘𝑍)) ∈ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ↔ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍))) | 
| 155 | 151, 154 | sylib 218 | . 2
⊢ (𝜑 → (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍))) | 
| 156 | 25 | simprd 495 | . . . . 5
⊢ (𝜑 → ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏)) | 
| 157 | 156 | simpld 494 | . . . 4
⊢ (𝜑 → (𝑊‘𝑍) We 𝑍) | 
| 158 |  | weso 5676 | . . . 4
⊢ ((𝑊‘𝑍) We 𝑍 → (𝑊‘𝑍) Or 𝑍) | 
| 159 | 157, 158 | syl 17 | . . 3
⊢ (𝜑 → (𝑊‘𝑍) Or 𝑍) | 
| 160 |  | sonr 5616 | . . 3
⊢ (((𝑊‘𝑍) Or 𝑍 ∧ (𝐻‘(card‘𝑍)) ∈ 𝑍) → ¬ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍))) | 
| 161 | 159, 109,
160 | syl2anc 584 | . 2
⊢ (𝜑 → ¬ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍))) | 
| 162 | 155, 161 | pm2.65i 194 | 1
⊢  ¬
𝜑 |