Metamath Proof Explorer

Theorem pwfseqlem4

Description: Lemma for pwfseq . Derive a final contradiction from the function F in pwfseqlem3 . Applying fpwwe2 to it, we get a certain maximal well-ordered subset Z , but the defining property ( Z F ( WZ ) ) e. Z contradicts our assumption on F , so we are reduced to the case of Z finite. This too is a contradiction, though, because Z and its preimage under ( WZ ) 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)

Ref Expression
Hypotheses 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 pwfseqlem4 ¬ 𝜑

Proof

Step Hyp Ref Expression
1 pwfseqlem4.g ⊢ ( 𝜑 → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
2 pwfseqlem4.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
3 pwfseqlem4.h ⊢ ( 𝜑 → 𝐻 : ω –1-1-onto→ 𝑋 )
4 pwfseqlem4.ps ⊢ ( 𝜓 ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) )
5 pwfseqlem4.k ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) –1-1→ 𝑥 )
6 pwfseqlem4.d ⊢ 𝐷 = ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } )
7 pwfseqlem4.f ⊢ 𝐹 = ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
8 pwfseqlem4.w ⊢ 𝑊 = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑏 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑏 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑏 ) ) }
9 pwfseqlem4.z ⊢ 𝑍 = ∪ dom 𝑊
10 eqid ⊢ 𝑍 = 𝑍
11 eqid ⊢ ( 𝑊 ‘ 𝑍 ) = ( 𝑊 ‘ 𝑍 )
12 10 11 pm3.2i ⊢ ( 𝑍 = 𝑍 ∧ ( 𝑊 ‘ 𝑍 ) = ( 𝑊 ‘ 𝑍 ) )
13 omex ⊢ ω ∈ V
14 ovex ⊢ ( 𝐴 ↑m 𝑛 ) ∈ V
15 13 14 iunex ⊢ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ V
16 f1dmex ⊢ ( ( 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ V ) → 𝒫 𝐴 ∈ V )
17 1 15 16 sylancl ⊢ ( 𝜑 → 𝒫 𝐴 ∈ V )
18 pwexb ⊢ ( 𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V )
19 17 18 sylibr ⊢ ( 𝜑 → 𝐴 ∈ V )
20 1 2 3 4 5 6 7 pwfseqlem4a ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 )
21 8 19 20 9 fpwwe2 ⊢ ( 𝜑 → ( ( 𝑍 𝑊 ( 𝑊 ‘ 𝑍 ) ∧ ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 ) ↔ ( 𝑍 = 𝑍 ∧ ( 𝑊 ‘ 𝑍 ) = ( 𝑊 ‘ 𝑍 ) ) ) )
22 12 21 mpbiri ⊢ ( 𝜑 → ( 𝑍 𝑊 ( 𝑊 ‘ 𝑍 ) ∧ ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 ) )
23 22 simpld ⊢ ( 𝜑 → 𝑍 𝑊 ( 𝑊 ‘ 𝑍 ) )
24 8 19 fpwwe2lem2 ⊢ ( 𝜑 → ( 𝑍 𝑊 ( 𝑊 ‘ 𝑍 ) ↔ ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) ∧ ( ( 𝑊 ‘ 𝑍 ) We 𝑍 ∧ ∀ 𝑏 ∈ 𝑍 [ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { 𝑏 } ) / 𝑣 ] ( 𝑣 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑏 ) ) ) )
25 23 24 mpbid ⊢ ( 𝜑 → ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) ∧ ( ( 𝑊 ‘ 𝑍 ) We 𝑍 ∧ ∀ 𝑏 ∈ 𝑍 [ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { 𝑏 } ) / 𝑣 ] ( 𝑣 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑏 ) ) )
26 id ⊢ ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
27 26 3expa ⊢ ( ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
28 27 adantrr ⊢ ( ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) ∧ ( ( 𝑊 ‘ 𝑍 ) We 𝑍 ∧ ∀ 𝑏 ∈ 𝑍 [ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { 𝑏 } ) / 𝑣 ] ( 𝑣 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑏 ) ) → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
29 25 28 syl ⊢ ( 𝜑 → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
30 22 simprd ⊢ ( 𝜑 → ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 )
31 25 simpld ⊢ ( 𝜑 → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) )
32 31 simpld ⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
33 19 32 ssexd ⊢ ( 𝜑 → 𝑍 ∈ V )
34 fvexd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑍 ) ∈ V )
35 simpl ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → 𝑎 = 𝑍 )
36 35 sseq1d ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( 𝑎 ⊆ 𝐴 ↔ 𝑍 ⊆ 𝐴 ) )
37 simpr ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → 𝑠 = ( 𝑊 ‘ 𝑍 ) )
38 35 sqxpeqd ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( 𝑎 × 𝑎 ) = ( 𝑍 × 𝑍 ) )
39 37 38 sseq12d ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( 𝑠 ⊆ ( 𝑎 × 𝑎 ) ↔ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) )
40 37 35 weeq12d ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( 𝑠 We 𝑎 ↔ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
41 36 39 40 3anbi123d ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ↔ ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) ) )
42 oveq12 ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( 𝑎 𝐹 𝑠 ) = ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) )
43 42 35 eleq12d ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 ↔ ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 ) )
44 35 breq1d ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( 𝑎 ≺ ω ↔ 𝑍 ≺ ω ) )
45 43 44 imbi12d ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( ( ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 → 𝑎 ≺ ω ) ↔ ( ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 → 𝑍 ≺ ω ) ) )
46 41 45 imbi12d ⊢ ( ( 𝑎 = 𝑍 ∧ 𝑠 = ( 𝑊 ‘ 𝑍 ) ) → ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) → ( ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 → 𝑎 ≺ ω ) ) ↔ ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) → ( ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 → 𝑍 ≺ ω ) ) ) )
47 omelon ⊢ ω ∈ On
48 onenon ⊢ ( ω ∈ On → ω ∈ dom card )
49 47 48 ax-mp ⊢ ω ∈ dom card
50 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → 𝑠 We 𝑎 )
51 50 19.8ad ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ∃ 𝑠 𝑠 We 𝑎 )
52 ween ⊢ ( 𝑎 ∈ dom card ↔ ∃ 𝑠 𝑠 We 𝑎 )
53 51 52 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → 𝑎 ∈ dom card )
54 domtri2 ⊢ ( ( ω ∈ dom card ∧ 𝑎 ∈ dom card ) → ( ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω ) )
55 49 53 54 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω ) )
56 nfv ⊢ Ⅎ 𝑟 ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) )
57 nfcv ⊢ Ⅎ 𝑟 𝑎
58 nfmpo2 ⊢ Ⅎ 𝑟 ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
59 7 58 nfcxfr ⊢ Ⅎ 𝑟 𝐹
60 nfcv ⊢ Ⅎ 𝑟 𝑠
61 57 59 60 nfov ⊢ Ⅎ 𝑟 ( 𝑎 𝐹 𝑠 )
62 61 nfel1 ⊢ Ⅎ 𝑟 ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 )
63 56 62 nfim ⊢ Ⅎ 𝑟 ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) )
64 sseq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 ⊆ ( 𝑎 × 𝑎 ) ↔ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) )
65 weeq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 We 𝑎 ↔ 𝑠 We 𝑎 ) )
66 64 65 3anbi23d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ↔ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) )
67 66 anbi1d ⊢ ( 𝑟 = 𝑠 → ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) )
68 67 anbi2d ⊢ ( 𝑟 = 𝑠 → ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) ↔ ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) ) )
69 oveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝑎 𝐹 𝑟 ) = ( 𝑎 𝐹 𝑠 ) )
70 69 eleq1d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ↔ ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) ) )
71 68 70 imbi12d ⊢ ( 𝑟 = 𝑠 → ( ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) ) ) )
72 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) )
73 nfcv ⊢ Ⅎ 𝑥 𝑎
74 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
75 7 74 nfcxfr ⊢ Ⅎ 𝑥 𝐹
76 nfcv ⊢ Ⅎ 𝑥 𝑟
77 73 75 76 nfov ⊢ Ⅎ 𝑥 ( 𝑎 𝐹 𝑟 )
78 77 nfel1 ⊢ Ⅎ 𝑥 ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 )
79 72 78 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) )
80 sseq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴 ) )
81 xpeq12 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑥 = 𝑎 ) → ( 𝑥 × 𝑥 ) = ( 𝑎 × 𝑎 ) )
82 81 anidms ⊢ ( 𝑥 = 𝑎 → ( 𝑥 × 𝑥 ) = ( 𝑎 × 𝑎 ) )
83 82 sseq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ) )
84 weeq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑟 We 𝑥 ↔ 𝑟 We 𝑎 ) )
85 80 83 84 3anbi123d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ↔ ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ) )
86 breq2 ⊢ ( 𝑥 = 𝑎 → ( ω ≼ 𝑥 ↔ ω ≼ 𝑎 ) )
87 85 86 anbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) )
88 4 87 bitrid ⊢ ( 𝑥 = 𝑎 → ( 𝜓 ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) )
89 88 anbi2d ⊢ ( 𝑥 = 𝑎 → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) ) )
90 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 𝐹 𝑟 ) = ( 𝑎 𝐹 𝑟 ) )
91 difeq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑎 ) )
92 90 91 eleq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) ↔ ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ) )
93 89 92 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ) ) )
94 1 2 3 4 5 6 7 pwfseqlem3 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) )
95 79 93 94 chvarfv ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) )
96 63 71 95 chvarfv ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) )
97 96 eldifbd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ¬ ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 )
98 97 expr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ω ≼ 𝑎 → ¬ ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 ) )
99 55 98 sylbird ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ¬ 𝑎 ≺ ω → ¬ ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 ) )
100 99 con4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 → 𝑎 ≺ ω ) )
101 100 ex ⊢ ( 𝜑 → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) → ( ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 → 𝑎 ≺ ω ) ) )
102 33 34 46 101 vtocl2d ⊢ ( 𝜑 → ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) → ( ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 → 𝑍 ≺ ω ) ) )
103 29 30 102 mp2d ⊢ ( 𝜑 → 𝑍 ≺ ω )
104 isfinite ⊢ ( 𝑍 ∈ Fin ↔ 𝑍 ≺ ω )
105 103 104 sylibr ⊢ ( 𝜑 → 𝑍 ∈ Fin )
106 fvex ⊢ ( 𝑊 ‘ 𝑍 ) ∈ V
107 1 2 3 4 5 6 7 pwfseqlem2 ⊢ ( ( 𝑍 ∈ Fin ∧ ( 𝑊 ‘ 𝑍 ) ∈ V ) → ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
108 105 106 107 sylancl ⊢ ( 𝜑 → ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
109 108 30 eqeltrrd ⊢ ( 𝜑 → ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ 𝑍 )
110 8 19 23 fpwwe2lem3 ⊢ ( ( 𝜑 ∧ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ 𝑍 ) → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ) = ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
111 109 110 mpdan ⊢ ( 𝜑 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ) = ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
112 cnvimass ⊢ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊆ dom ( 𝑊 ‘ 𝑍 )
113 31 simprd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) )
114 dmss ⊢ ( ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) → dom ( 𝑊 ‘ 𝑍 ) ⊆ dom ( 𝑍 × 𝑍 ) )
115 113 114 syl ⊢ ( 𝜑 → dom ( 𝑊 ‘ 𝑍 ) ⊆ dom ( 𝑍 × 𝑍 ) )
116 dmxpss ⊢ dom ( 𝑍 × 𝑍 ) ⊆ 𝑍
117 115 116 sstrdi ⊢ ( 𝜑 → dom ( 𝑊 ‘ 𝑍 ) ⊆ 𝑍 )
118 112 117 sstrid ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊆ 𝑍 )
119 105 118 ssfid ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ Fin )
120 106 inex1 ⊢ ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ∈ V
121 1 2 3 4 5 6 7 pwfseqlem2 ⊢ ( ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ Fin ∧ ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ∈ V ) → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
122 119 120 121 sylancl ⊢ ( 𝜑 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
123 111 122 eqtr3d ⊢ ( 𝜑 → ( 𝐻 ‘ ( card ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
124 f1of1 ⊢ ( 𝐻 : ω –1-1-onto→ 𝑋 → 𝐻 : ω –1-1→ 𝑋 )
125 3 124 syl ⊢ ( 𝜑 → 𝐻 : ω –1-1→ 𝑋 )
126 ficardom ⊢ ( 𝑍 ∈ Fin → ( card ‘ 𝑍 ) ∈ ω )
127 105 126 syl ⊢ ( 𝜑 → ( card ‘ 𝑍 ) ∈ ω )
128 ficardom ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ Fin → ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ∈ ω )
129 119 128 syl ⊢ ( 𝜑 → ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ∈ ω )
130 f1fveq ⊢ ( ( 𝐻 : ω –1-1→ 𝑋 ∧ ( ( card ‘ 𝑍 ) ∈ ω ∧ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ∈ ω ) ) → ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ↔ ( card ‘ 𝑍 ) = ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
131 125 127 129 130 syl12anc ⊢ ( 𝜑 → ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ↔ ( card ‘ 𝑍 ) = ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
132 123 131 mpbid ⊢ ( 𝜑 → ( card ‘ 𝑍 ) = ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) )
133 132 eqcomd ⊢ ( 𝜑 → ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) = ( card ‘ 𝑍 ) )
134 finnum ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ Fin → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ dom card )
135 119 134 syl ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ dom card )
136 finnum ⊢ ( 𝑍 ∈ Fin → 𝑍 ∈ dom card )
137 105 136 syl ⊢ ( 𝜑 → 𝑍 ∈ dom card )
138 carden2 ⊢ ( ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ dom card ∧ 𝑍 ∈ dom card ) → ( ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) = ( card ‘ 𝑍 ) ↔ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
139 135 137 138 syl2anc ⊢ ( 𝜑 → ( ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) = ( card ‘ 𝑍 ) ↔ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
140 133 139 mpbid ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 )
141 dfpss2 ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ↔ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊆ 𝑍 ∧ ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 ) )
142 141 baib ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊆ 𝑍 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ↔ ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 ) )
143 118 142 syl ⊢ ( 𝜑 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ↔ ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 ) )
144 php3 ⊢ ( ( 𝑍 ∈ Fin ∧ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ) → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≺ 𝑍 )
145 sdomnen ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≺ 𝑍 → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 )
146 144 145 syl ⊢ ( ( 𝑍 ∈ Fin ∧ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ) → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 )
147 146 ex ⊢ ( 𝑍 ∈ Fin → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
148 105 147 syl ⊢ ( 𝜑 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
149 143 148 sylbird ⊢ ( 𝜑 → ( ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
150 140 149 mt4d ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 )
151 109 150 eleqtrrd ⊢ ( 𝜑 → ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) )
152 fvex ⊢ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ V
153 152 eliniseg ⊢ ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ V → ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ↔ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ) )
154 152 153 ax-mp ⊢ ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ↔ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
155 151 154 sylib ⊢ ( 𝜑 → ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
156 25 simprd ⊢ ( 𝜑 → ( ( 𝑊 ‘ 𝑍 ) We 𝑍 ∧ ∀ 𝑏 ∈ 𝑍 [ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { 𝑏 } ) / 𝑣 ] ( 𝑣 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑏 ) )
157 156 simpld ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑍 ) We 𝑍 )
158 weso ⊢ ( ( 𝑊 ‘ 𝑍 ) We 𝑍 → ( 𝑊 ‘ 𝑍 ) Or 𝑍 )
159 157 158 syl ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑍 ) Or 𝑍 )
160 sonr ⊢ ( ( ( 𝑊 ‘ 𝑍 ) Or 𝑍 ∧ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ 𝑍 ) → ¬ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
161 159 109 160 syl2anc ⊢ ( 𝜑 → ¬ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
162 155 161 pm2.65i ⊢ ¬ 𝜑