MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwfseqlem4 Structured version   Visualization version   GIF version

Theorem pwfseqlem4 10700
Description: Lemma for pwfseq 10702. Derive a final contradiction from the function 𝐹 in pwfseqlem3 10698. Applying fpwwe2 10681 to it, we get a certain maximal well-ordered subset 𝑍, but the defining property (𝑍𝐹(𝑊𝑍)) ∈ 𝑍 contradicts our assumption on 𝐹, so we are reduced to the case of 𝑍 finite. This too is a contradiction, though, because 𝑍 and its preimage under (𝑊𝑍) are distinct sets of the same cardinality and in a subset relation, which is impossible for finite sets. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by Matthew House, 10-Sep-2025.)
Hypotheses
Ref Expression
pwfseqlem4.g (𝜑𝐺:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛))
pwfseqlem4.x (𝜑𝑋𝐴)
pwfseqlem4.h (𝜑𝐻:ω–1-1-onto𝑋)
pwfseqlem4.ps (𝜓 ↔ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))
pwfseqlem4.k ((𝜑𝜓) → 𝐾: 𝑛 ∈ ω (𝑥m 𝑛)–1-1𝑥)
pwfseqlem4.d 𝐷 = (𝐺‘{𝑤𝑥 ∣ ((𝐾𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (𝐺‘(𝐾𝑤)))})
pwfseqlem4.f 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷 {𝑧 ∈ ω ∣ ¬ (𝐷𝑧) ∈ 𝑥})))
pwfseqlem4.w 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏𝑎 [(𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))}
pwfseqlem4.z 𝑍 = dom 𝑊
Assertion
Ref Expression
pwfseqlem4 ¬ 𝜑
Distinct variable groups:   𝑛,𝑟,𝑤,𝑥,𝑧   𝐷,𝑛,𝑧   𝑎,𝑏,𝑠,𝑣,𝐹   𝑤,𝐺   𝑤,𝐾   𝑟,𝑎,𝑥,𝑧,𝐻,𝑏,𝑠,𝑣   𝑛,𝑎,𝜑,𝑏,𝑠,𝑣,𝑟,𝑥,𝑧   𝜓,𝑛,𝑧   𝐴,𝑎,𝑛,𝑟,𝑠,𝑥,𝑧   𝑊,𝑎,𝑏,𝑠,𝑣   𝑍,𝑎,𝑏,𝑠,𝑣
Allowed substitution hints:   𝜑(𝑤)   𝜓(𝑥,𝑤,𝑣,𝑠,𝑟,𝑎,𝑏)   𝐴(𝑤,𝑣,𝑏)   𝐷(𝑥,𝑤,𝑣,𝑠,𝑟,𝑎,𝑏)   𝐹(𝑥,𝑧,𝑤,𝑛,𝑟)   𝐺(𝑥,𝑧,𝑣,𝑛,𝑠,𝑟,𝑎,𝑏)   𝐻(𝑤,𝑛)   𝐾(𝑥,𝑧,𝑣,𝑛,𝑠,𝑟,𝑎,𝑏)   𝑊(𝑥,𝑧,𝑤,𝑛,𝑟)   𝑋(𝑥,𝑧,𝑤,𝑣,𝑛,𝑠,𝑟,𝑎,𝑏)   𝑍(𝑥,𝑧,𝑤,𝑛,𝑟)

Proof of Theorem pwfseqlem4
StepHypRef Expression
1 eqid 2735 . . . . . . . . . . . . 13 𝑍 = 𝑍
2 eqid 2735 . . . . . . . . . . . . 13 (𝑊𝑍) = (𝑊𝑍)
31, 2pm3.2i 470 . . . . . . . . . . . 12 (𝑍 = 𝑍 ∧ (𝑊𝑍) = (𝑊𝑍))
4 pwfseqlem4.w . . . . . . . . . . . . 13 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏𝑎 [(𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))}
5 pwfseqlem4.g . . . . . . . . . . . . . . 15 (𝜑𝐺:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛))
6 omex 9681 . . . . . . . . . . . . . . . 16 ω ∈ V
7 ovex 7464 . . . . . . . . . . . . . . . 16 (𝐴m 𝑛) ∈ V
86, 7iunex 7992 . . . . . . . . . . . . . . 15 𝑛 ∈ ω (𝐴m 𝑛) ∈ V
9 f1dmex 7980 . . . . . . . . . . . . . . 15 ((𝐺:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴m 𝑛) ∧ 𝑛 ∈ ω (𝐴m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
105, 8, 9sylancl 586 . . . . . . . . . . . . . 14 (𝜑 → 𝒫 𝐴 ∈ V)
11 pwexb 7785 . . . . . . . . . . . . . 14 (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
1210, 11sylibr 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‘𝑥)), (𝐷 {𝑧 ∈ ω ∣ ¬ (𝐷𝑧) ∈ 𝑥})))
195, 13, 14, 15, 16, 17, 18pwfseqlem4a 10699 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴)
20 pwfseqlem4.z . . . . . . . . . . . . 13 𝑍 = dom 𝑊
214, 12, 19, 20fpwwe2 10681 . . . . . . . . . . . 12 (𝜑 → ((𝑍𝑊(𝑊𝑍) ∧ (𝑍𝐹(𝑊𝑍)) ∈ 𝑍) ↔ (𝑍 = 𝑍 ∧ (𝑊𝑍) = (𝑊𝑍))))
223, 21mpbiri 258 . . . . . . . . . . 11 (𝜑 → (𝑍𝑊(𝑊𝑍) ∧ (𝑍𝐹(𝑊𝑍)) ∈ 𝑍))
2322simpld 494 . . . . . . . . . 10 (𝜑𝑍𝑊(𝑊𝑍))
244, 12fpwwe2lem2 10670 . . . . . . . . . 10 (𝜑 → (𝑍𝑊(𝑊𝑍) ↔ ((𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊𝑍) We 𝑍 ∧ ∀𝑏𝑍 [((𝑊𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊𝑍) ∩ (𝑣 × 𝑣))) = 𝑏))))
2523, 24mpbid 232 . . . . . . . . 9 (𝜑 → ((𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊𝑍) We 𝑍 ∧ ∀𝑏𝑍 [((𝑊𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊𝑍) ∩ (𝑣 × 𝑣))) = 𝑏)))
26 id 22 . . . . . . . . . . 11 ((𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊𝑍) We 𝑍) → (𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊𝑍) We 𝑍))
27263expa 1117 . . . . . . . . . 10 (((𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍)) ∧ (𝑊𝑍) We 𝑍) → (𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊𝑍) We 𝑍))
2827adantrr 717 . . . . . . . . 9 (((𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊𝑍) We 𝑍 ∧ ∀𝑏𝑍 [((𝑊𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊𝑍) ∩ (𝑣 × 𝑣))) = 𝑏)) → (𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊𝑍) We 𝑍))
2925, 28syl 17 . . . . . . . 8 (𝜑 → (𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊𝑍) We 𝑍))
3022simprd 495 . . . . . . . 8 (𝜑 → (𝑍𝐹(𝑊𝑍)) ∈ 𝑍)
3125simpld 494 . . . . . . . . . . 11 (𝜑 → (𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍)))
3231simpld 494 . . . . . . . . . 10 (𝜑𝑍𝐴)
3312, 32ssexd 5330 . . . . . . . . 9 (𝜑𝑍 ∈ V)
34 fvexd 6922 . . . . . . . . 9 (𝜑 → (𝑊𝑍) ∈ V)
35 simpl 482 . . . . . . . . . . . 12 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → 𝑎 = 𝑍)
3635sseq1d 4027 . . . . . . . . . . 11 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → (𝑎𝐴𝑍𝐴))
37 simpr 484 . . . . . . . . . . . 12 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → 𝑠 = (𝑊𝑍))
3835sqxpeqd 5721 . . . . . . . . . . . 12 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → (𝑎 × 𝑎) = (𝑍 × 𝑍))
3937, 38sseq12d 4029 . . . . . . . . . . 11 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → (𝑠 ⊆ (𝑎 × 𝑎) ↔ (𝑊𝑍) ⊆ (𝑍 × 𝑍)))
4037, 35weeq12d 5678 . . . . . . . . . . 11 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → (𝑠 We 𝑎 ↔ (𝑊𝑍) We 𝑍))
4136, 39, 403anbi123d 1435 . . . . . . . . . 10 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ↔ (𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊𝑍) We 𝑍)))
42 oveq12 7440 . . . . . . . . . . . 12 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → (𝑎𝐹𝑠) = (𝑍𝐹(𝑊𝑍)))
4342, 35eleq12d 2833 . . . . . . . . . . 11 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → ((𝑎𝐹𝑠) ∈ 𝑎 ↔ (𝑍𝐹(𝑊𝑍)) ∈ 𝑍))
4435breq1d 5158 . . . . . . . . . . 11 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → (𝑎 ≺ ω ↔ 𝑍 ≺ ω))
4543, 44imbi12d 344 . . . . . . . . . 10 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → (((𝑎𝐹𝑠) ∈ 𝑎𝑎 ≺ ω) ↔ ((𝑍𝐹(𝑊𝑍)) ∈ 𝑍𝑍 ≺ ω)))
4641, 45imbi12d 344 . . . . . . . . 9 ((𝑎 = 𝑍𝑠 = (𝑊𝑍)) → (((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) → ((𝑎𝐹𝑠) ∈ 𝑎𝑎 ≺ ω)) ↔ ((𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊𝑍) We 𝑍) → ((𝑍𝐹(𝑊𝑍)) ∈ 𝑍𝑍 ≺ ω))))
47 omelon 9684 . . . . . . . . . . . . . 14 ω ∈ On
48 onenon 9987 . . . . . . . . . . . . . 14 (ω ∈ On → ω ∈ dom card)
4947, 48ax-mp 5 . . . . . . . . . . . . 13 ω ∈ dom card
50 simpr3 1195 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑠 We 𝑎)
515019.8ad 2180 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ∃𝑠 𝑠 We 𝑎)
52 ween 10073 . . . . . . . . . . . . . 14 (𝑎 ∈ dom card ↔ ∃𝑠 𝑠 We 𝑎)
5351, 52sylibr 234 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑎 ∈ dom card)
54 domtri2 10027 . . . . . . . . . . . . 13 ((ω ∈ dom card ∧ 𝑎 ∈ dom card) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω))
5549, 53, 54sylancr 587 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω))
56 nfv 1912 . . . . . . . . . . . . . . . 16 𝑟(𝜑 ∧ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎))
57 nfcv 2903 . . . . . . . . . . . . . . . . . 18 𝑟𝑎
58 nfmpo2 7514 . . . . . . . . . . . . . . . . . . 19 𝑟(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷 {𝑧 ∈ ω ∣ ¬ (𝐷𝑧) ∈ 𝑥})))
5918, 58nfcxfr 2901 . . . . . . . . . . . . . . . . . 18 𝑟𝐹
60 nfcv 2903 . . . . . . . . . . . . . . . . . 18 𝑟𝑠
6157, 59, 60nfov 7461 . . . . . . . . . . . . . . . . 17 𝑟(𝑎𝐹𝑠)
6261nfel1 2920 . . . . . . . . . . . . . . . 16 𝑟(𝑎𝐹𝑠) ∈ (𝐴𝑎)
6356, 62nfim 1894 . . . . . . . . . . . . . . 15 𝑟((𝜑 ∧ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴𝑎))
64 sseq1 4021 . . . . . . . . . . . . . . . . . . 19 (𝑟 = 𝑠 → (𝑟 ⊆ (𝑎 × 𝑎) ↔ 𝑠 ⊆ (𝑎 × 𝑎)))
65 weeq1 5676 . . . . . . . . . . . . . . . . . . 19 (𝑟 = 𝑠 → (𝑟 We 𝑎𝑠 We 𝑎))
6664, 653anbi23d 1438 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ↔ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)))
6766anbi1d 631 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → (((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎) ↔ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)))
6867anbi2d 630 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑠 → ((𝜑 ∧ ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) ↔ (𝜑 ∧ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎))))
69 oveq2 7439 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → (𝑎𝐹𝑟) = (𝑎𝐹𝑠))
7069eleq1d 2824 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑠 → ((𝑎𝐹𝑟) ∈ (𝐴𝑎) ↔ (𝑎𝐹𝑠) ∈ (𝐴𝑎)))
7168, 70imbi12d 344 . . . . . . . . . . . . . . 15 (𝑟 = 𝑠 → (((𝜑 ∧ ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴𝑎)) ↔ ((𝜑 ∧ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴𝑎))))
72 nfv 1912 . . . . . . . . . . . . . . . . 17 𝑥(𝜑 ∧ ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))
73 nfcv 2903 . . . . . . . . . . . . . . . . . . 19 𝑥𝑎
74 nfmpo1 7513 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷 {𝑧 ∈ ω ∣ ¬ (𝐷𝑧) ∈ 𝑥})))
7518, 74nfcxfr 2901 . . . . . . . . . . . . . . . . . . 19 𝑥𝐹
76 nfcv 2903 . . . . . . . . . . . . . . . . . . 19 𝑥𝑟
7773, 75, 76nfov 7461 . . . . . . . . . . . . . . . . . 18 𝑥(𝑎𝐹𝑟)
7877nfel1 2920 . . . . . . . . . . . . . . . . 17 𝑥(𝑎𝐹𝑟) ∈ (𝐴𝑎)
7972, 78nfim 1894 . . . . . . . . . . . . . . . 16 𝑥((𝜑 ∧ ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴𝑎))
80 sseq1 4021 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑎 → (𝑥𝐴𝑎𝐴))
81 xpeq12 5714 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = 𝑎𝑥 = 𝑎) → (𝑥 × 𝑥) = (𝑎 × 𝑎))
8281anidms 566 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎 → (𝑥 × 𝑥) = (𝑎 × 𝑎))
8382sseq2d 4028 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑎 → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑟 ⊆ (𝑎 × 𝑎)))
84 weeq2 5677 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑎 → (𝑟 We 𝑥𝑟 We 𝑎))
8580, 83, 843anbi123d 1435 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑎 → ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎)))
86 breq2 5152 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑎 → (ω ≼ 𝑥 ↔ ω ≼ 𝑎))
8785, 86anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → (((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥) ↔ ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)))
8815, 87bitrid 283 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (𝜓 ↔ ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)))
8988anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))))
90 oveq1 7438 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (𝑥𝐹𝑟) = (𝑎𝐹𝑟))
91 difeq2 4130 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (𝐴𝑥) = (𝐴𝑎))
9290, 91eleq12d 2833 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → ((𝑥𝐹𝑟) ∈ (𝐴𝑥) ↔ (𝑎𝐹𝑟) ∈ (𝐴𝑎)))
9389, 92imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (((𝜑𝜓) → (𝑥𝐹𝑟) ∈ (𝐴𝑥)) ↔ ((𝜑 ∧ ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴𝑎))))
945, 13, 14, 15, 16, 17, 18pwfseqlem3 10698 . . . . . . . . . . . . . . . 16 ((𝜑𝜓) → (𝑥𝐹𝑟) ∈ (𝐴𝑥))
9579, 93, 94chvarfv 2238 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎𝐴𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴𝑎))
9663, 71, 95chvarfv 2238 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴𝑎))
9796eldifbd 3976 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → ¬ (𝑎𝐹𝑠) ∈ 𝑎)
9897expr 456 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 → ¬ (𝑎𝐹𝑠) ∈ 𝑎))
9955, 98sylbird 260 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (¬ 𝑎 ≺ ω → ¬ (𝑎𝐹𝑠) ∈ 𝑎))
10099con4d 115 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ((𝑎𝐹𝑠) ∈ 𝑎𝑎 ≺ ω))
101100ex 412 . . . . . . . . 9 (𝜑 → ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) → ((𝑎𝐹𝑠) ∈ 𝑎𝑎 ≺ ω)))
10233, 34, 46, 101vtocl2d 3562 . . . . . . . 8 (𝜑 → ((𝑍𝐴 ∧ (𝑊𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊𝑍) We 𝑍) → ((𝑍𝐹(𝑊𝑍)) ∈ 𝑍𝑍 ≺ ω)))
10329, 30, 102mp2d 49 . . . . . . 7 (𝜑𝑍 ≺ ω)
104 isfinite 9690 . . . . . . 7 (𝑍 ∈ Fin ↔ 𝑍 ≺ ω)
105103, 104sylibr 234 . . . . . 6 (𝜑𝑍 ∈ Fin)
106 fvex 6920 . . . . . 6 (𝑊𝑍) ∈ V
1075, 13, 14, 15, 16, 17, 18pwfseqlem2 10697 . . . . . 6 ((𝑍 ∈ Fin ∧ (𝑊𝑍) ∈ V) → (𝑍𝐹(𝑊𝑍)) = (𝐻‘(card‘𝑍)))
108105, 106, 107sylancl 586 . . . . 5 (𝜑 → (𝑍𝐹(𝑊𝑍)) = (𝐻‘(card‘𝑍)))
109108, 30eqeltrrd 2840 . . . 4 (𝜑 → (𝐻‘(card‘𝑍)) ∈ 𝑍)
1104, 12, 23fpwwe2lem3 10671 . . . . . . . . . 10 ((𝜑 ∧ (𝐻‘(card‘𝑍)) ∈ 𝑍) → (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊𝑍) ∩ (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) × ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘𝑍)))
111109, 110mpdan 687 . . . . . . . . 9 (𝜑 → (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊𝑍) ∩ (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) × ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘𝑍)))
112 cnvimass 6102 . . . . . . . . . . . 12 ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ dom (𝑊𝑍)
11331simprd 495 . . . . . . . . . . . . . 14 (𝜑 → (𝑊𝑍) ⊆ (𝑍 × 𝑍))
114 dmss 5916 . . . . . . . . . . . . . 14 ((𝑊𝑍) ⊆ (𝑍 × 𝑍) → dom (𝑊𝑍) ⊆ dom (𝑍 × 𝑍))
115113, 114syl 17 . . . . . . . . . . . . 13 (𝜑 → dom (𝑊𝑍) ⊆ dom (𝑍 × 𝑍))
116 dmxpss 6193 . . . . . . . . . . . . 13 dom (𝑍 × 𝑍) ⊆ 𝑍
117115, 116sstrdi 4008 . . . . . . . . . . . 12 (𝜑 → dom (𝑊𝑍) ⊆ 𝑍)
118112, 117sstrid 4007 . . . . . . . . . . 11 (𝜑 → ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍)
119105, 118ssfid 9299 . . . . . . . . . 10 (𝜑 → ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin)
120106inex1 5323 . . . . . . . . . 10 ((𝑊𝑍) ∩ (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) × ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))) ∈ V
1215, 13, 14, 15, 16, 17, 18pwfseqlem2 10697 . . . . . . . . . 10 ((((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin ∧ ((𝑊𝑍) ∩ (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) × ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))) ∈ V) → (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊𝑍) ∩ (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) × ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))))
122119, 120, 121sylancl 586 . . . . . . . . 9 (𝜑 → (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊𝑍) ∩ (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) × ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))))
123111, 122eqtr3d 2777 . . . . . . . 8 (𝜑 → (𝐻‘(card‘𝑍)) = (𝐻‘(card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))))
124 f1of1 6848 . . . . . . . . . 10 (𝐻:ω–1-1-onto𝑋𝐻:ω–1-1𝑋)
12514, 124syl 17 . . . . . . . . 9 (𝜑𝐻:ω–1-1𝑋)
126 ficardom 9999 . . . . . . . . . 10 (𝑍 ∈ Fin → (card‘𝑍) ∈ ω)
127105, 126syl 17 . . . . . . . . 9 (𝜑 → (card‘𝑍) ∈ ω)
128 ficardom 9999 . . . . . . . . . 10 (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin → (card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)
129119, 128syl 17 . . . . . . . . 9 (𝜑 → (card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)
130 f1fveq 7282 . . . . . . . . 9 ((𝐻:ω–1-1𝑋 ∧ ((card‘𝑍) ∈ ω ∧ (card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)) → ((𝐻‘(card‘𝑍)) = (𝐻‘(card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))) ↔ (card‘𝑍) = (card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))))
131125, 127, 129, 130syl12anc 837 . . . . . . . 8 (𝜑 → ((𝐻‘(card‘𝑍)) = (𝐻‘(card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))) ↔ (card‘𝑍) = (card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))))
132123, 131mpbid 232 . . . . . . 7 (𝜑 → (card‘𝑍) = (card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})))
133132eqcomd 2741 . . . . . 6 (𝜑 → (card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍))
134 finnum 9986 . . . . . . . 8 (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin → ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card)
135119, 134syl 17 . . . . . . 7 (𝜑 → ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card)
136 finnum 9986 . . . . . . . 8 (𝑍 ∈ Fin → 𝑍 ∈ dom card)
137105, 136syl 17 . . . . . . 7 (𝜑𝑍 ∈ dom card)
138 carden2 10025 . . . . . . 7 ((((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card ∧ 𝑍 ∈ dom card) → ((card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍) ↔ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
139135, 137, 138syl2anc 584 . . . . . 6 (𝜑 → ((card‘((𝑊𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍) ↔ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
140133, 139mpbid 232 . . . . 5 (𝜑 → ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)
141 dfpss2 4098 . . . . . . . 8 (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍 ∧ ¬ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍))
142141baib 535 . . . . . . 7 (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍 → (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ¬ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍))
143118, 142syl 17 . . . . . 6 (𝜑 → (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ¬ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍))
144 php3 9247 . . . . . . . . 9 ((𝑍 ∈ Fin ∧ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍) → ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≺ 𝑍)
145 sdomnen 9020 . . . . . . . . 9 (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≺ 𝑍 → ¬ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)
146144, 145syl 17 . . . . . . . 8 ((𝑍 ∈ Fin ∧ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍) → ¬ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)
147146ex 412 . . . . . . 7 (𝑍 ∈ Fin → (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 → ¬ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
148105, 147syl 17 . . . . . 6 (𝜑 → (((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 → ¬ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
149143, 148sylbird 260 . . . . 5 (𝜑 → (¬ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍 → ¬ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
150140, 149mt4d 117 . . . 4 (𝜑 → ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍)
151109, 150eleqtrrd 2842 . . 3 (𝜑 → (𝐻‘(card‘𝑍)) ∈ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}))
152 fvex 6920 . . . 4 (𝐻‘(card‘𝑍)) ∈ V
153152eliniseg 6115 . . . 4 ((𝐻‘(card‘𝑍)) ∈ V → ((𝐻‘(card‘𝑍)) ∈ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ↔ (𝐻‘(card‘𝑍))(𝑊𝑍)(𝐻‘(card‘𝑍))))
154152, 153ax-mp 5 . . 3 ((𝐻‘(card‘𝑍)) ∈ ((𝑊𝑍) “ {(𝐻‘(card‘𝑍))}) ↔ (𝐻‘(card‘𝑍))(𝑊𝑍)(𝐻‘(card‘𝑍)))
155151, 154sylib 218 . 2 (𝜑 → (𝐻‘(card‘𝑍))(𝑊𝑍)(𝐻‘(card‘𝑍)))
15625simprd 495 . . . . 5 (𝜑 → ((𝑊𝑍) We 𝑍 ∧ ∀𝑏𝑍 [((𝑊𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊𝑍) ∩ (𝑣 × 𝑣))) = 𝑏))
157156simpld 494 . . . 4 (𝜑 → (𝑊𝑍) We 𝑍)
158 weso 5680 . . . 4 ((𝑊𝑍) We 𝑍 → (𝑊𝑍) Or 𝑍)
159157, 158syl 17 . . 3 (𝜑 → (𝑊𝑍) Or 𝑍)
160 sonr 5621 . . 3 (((𝑊𝑍) Or 𝑍 ∧ (𝐻‘(card‘𝑍)) ∈ 𝑍) → ¬ (𝐻‘(card‘𝑍))(𝑊𝑍)(𝐻‘(card‘𝑍)))
161159, 109, 160syl2anc 584 . 2 (𝜑 → ¬ (𝐻‘(card‘𝑍))(𝑊𝑍)(𝐻‘(card‘𝑍)))
162155, 161pm2.65i 194 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wex 1776  wcel 2106  wral 3059  {crab 3433  Vcvv 3478  [wsbc 3791  cdif 3960  cin 3962  wss 3963  wpss 3964  ifcif 4531  𝒫 cpw 4605  {csn 4631   cuni 4912   cint 4951   ciun 4996   class class class wbr 5148  {copab 5210   Or wor 5596   We wwe 5640   × cxp 5687  ccnv 5688  dom cdm 5689  ran crn 5690  cima 5692  Oncon0 6386  1-1wf1 6560  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  cmpo 7433  ωcom 7887  m cmap 8865  cen 8981  cdom 8982  csdm 8983  Fincfn 8984  cardccrd 9973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-oi 9548  df-card 9977
This theorem is referenced by:  pwfseqlem5  10701
  Copyright terms: Public domain W3C validator