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)

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 simprd ⊢ ( 𝜑 → ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 )
24 22 simpld ⊢ ( 𝜑 → 𝑍 𝑊 ( 𝑊 ‘ 𝑍 ) )
25 8 19 fpwwe2lem2 ⊢ ( 𝜑 → ( 𝑍 𝑊 ( 𝑊 ‘ 𝑍 ) ↔ ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) ∧ ( ( 𝑊 ‘ 𝑍 ) We 𝑍 ∧ ∀ 𝑏 ∈ 𝑍 [ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { 𝑏 } ) / 𝑣 ] ( 𝑣 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑏 ) ) ) )
26 24 25 mpbid ⊢ ( 𝜑 → ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) ∧ ( ( 𝑊 ‘ 𝑍 ) We 𝑍 ∧ ∀ 𝑏 ∈ 𝑍 [ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { 𝑏 } ) / 𝑣 ] ( 𝑣 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑏 ) ) )
27 26 simpld ⊢ ( 𝜑 → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) )
28 27 simpld ⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
29 19 28 ssexd ⊢ ( 𝜑 → 𝑍 ∈ V )
30 sseq1 ⊢ ( 𝑎 = 𝑍 → ( 𝑎 ⊆ 𝐴 ↔ 𝑍 ⊆ 𝐴 ) )
31 id ⊢ ( 𝑎 = 𝑍 → 𝑎 = 𝑍 )
32 31 sqxpeqd ⊢ ( 𝑎 = 𝑍 → ( 𝑎 × 𝑎 ) = ( 𝑍 × 𝑍 ) )
33 32 sseq2d ⊢ ( 𝑎 = 𝑍 → ( ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ↔ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) )
34 weeq2 ⊢ ( 𝑎 = 𝑍 → ( ( 𝑊 ‘ 𝑍 ) We 𝑎 ↔ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
35 30 33 34 3anbi123d ⊢ ( 𝑎 = 𝑍 → ( ( 𝑎 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑎 ) ↔ ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) ) )
36 35 anbi2d ⊢ ( 𝑎 = 𝑍 → ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑎 ) ) ↔ ( 𝜑 ∧ ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) ) ) )
37 id ⊢ ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
38 37 3expa ⊢ ( ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
39 38 adantrr ⊢ ( ( ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ) ∧ ( ( 𝑊 ‘ 𝑍 ) We 𝑍 ∧ ∀ 𝑏 ∈ 𝑍 [ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { 𝑏 } ) / 𝑣 ] ( 𝑣 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑏 ) ) → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
40 26 39 syl ⊢ ( 𝜑 → ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) )
41 40 pm4.71i ⊢ ( 𝜑 ↔ ( 𝜑 ∧ ( 𝑍 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑍 ) ) )
42 36 41 bitr4di ⊢ ( 𝑎 = 𝑍 → ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑎 ) ) ↔ 𝜑 ) )
43 oveq1 ⊢ ( 𝑎 = 𝑍 → ( 𝑎 𝐹 ( 𝑊 ‘ 𝑍 ) ) = ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) )
44 43 31 eleq12d ⊢ ( 𝑎 = 𝑍 → ( ( 𝑎 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑎 ↔ ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 ) )
45 breq1 ⊢ ( 𝑎 = 𝑍 → ( 𝑎 ≺ ω ↔ 𝑍 ≺ ω ) )
46 44 45 imbi12d ⊢ ( 𝑎 = 𝑍 → ( ( ( 𝑎 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑎 → 𝑎 ≺ ω ) ↔ ( ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 → 𝑍 ≺ ω ) ) )
47 42 46 imbi12d ⊢ ( 𝑎 = 𝑍 → ( ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑎 ) ) → ( ( 𝑎 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑎 → 𝑎 ≺ ω ) ) ↔ ( 𝜑 → ( ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 → 𝑍 ≺ ω ) ) ) )
48 fvex ⊢ ( 𝑊 ‘ 𝑍 ) ∈ V
49 sseq1 ⊢ ( 𝑠 = ( 𝑊 ‘ 𝑍 ) → ( 𝑠 ⊆ ( 𝑎 × 𝑎 ) ↔ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ) )
50 weeq1 ⊢ ( 𝑠 = ( 𝑊 ‘ 𝑍 ) → ( 𝑠 We 𝑎 ↔ ( 𝑊 ‘ 𝑍 ) We 𝑎 ) )
51 49 50 3anbi23d ⊢ ( 𝑠 = ( 𝑊 ‘ 𝑍 ) → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ↔ ( 𝑎 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑎 ) ) )
52 51 anbi2d ⊢ ( 𝑠 = ( 𝑊 ‘ 𝑍 ) → ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) ↔ ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑎 ) ) ) )
53 oveq2 ⊢ ( 𝑠 = ( 𝑊 ‘ 𝑍 ) → ( 𝑎 𝐹 𝑠 ) = ( 𝑎 𝐹 ( 𝑊 ‘ 𝑍 ) ) )
54 53 eleq1d ⊢ ( 𝑠 = ( 𝑊 ‘ 𝑍 ) → ( ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 ↔ ( 𝑎 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑎 ) )
55 54 imbi1d ⊢ ( 𝑠 = ( 𝑊 ‘ 𝑍 ) → ( ( ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 → 𝑎 ≺ ω ) ↔ ( ( 𝑎 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑎 → 𝑎 ≺ ω ) ) )
56 52 55 imbi12d ⊢ ( 𝑠 = ( 𝑊 ‘ 𝑍 ) → ( ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 → 𝑎 ≺ ω ) ) ↔ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑎 ) ) → ( ( 𝑎 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑎 → 𝑎 ≺ ω ) ) ) )
57 omelon ⊢ ω ∈ On
58 onenon ⊢ ( ω ∈ On → ω ∈ dom card )
59 57 58 ax-mp ⊢ ω ∈ dom card
60 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → 𝑠 We 𝑎 )
61 60 19.8ad ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ∃ 𝑠 𝑠 We 𝑎 )
62 ween ⊢ ( 𝑎 ∈ dom card ↔ ∃ 𝑠 𝑠 We 𝑎 )
63 61 62 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → 𝑎 ∈ dom card )
64 domtri2 ⊢ ( ( ω ∈ dom card ∧ 𝑎 ∈ dom card ) → ( ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω ) )
65 59 63 64 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω ) )
66 nfv ⊢ Ⅎ 𝑟 ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) )
67 nfcv ⊢ Ⅎ 𝑟 𝑎
68 nfmpo2 ⊢ Ⅎ 𝑟 ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
69 7 68 nfcxfr ⊢ Ⅎ 𝑟 𝐹
70 nfcv ⊢ Ⅎ 𝑟 𝑠
71 67 69 70 nfov ⊢ Ⅎ 𝑟 ( 𝑎 𝐹 𝑠 )
72 71 nfel1 ⊢ Ⅎ 𝑟 ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 )
73 66 72 nfim ⊢ Ⅎ 𝑟 ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) )
74 sseq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 ⊆ ( 𝑎 × 𝑎 ) ↔ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) )
75 weeq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 We 𝑎 ↔ 𝑠 We 𝑎 ) )
76 74 75 3anbi23d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ↔ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) )
77 76 anbi1d ⊢ ( 𝑟 = 𝑠 → ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) )
78 77 anbi2d ⊢ ( 𝑟 = 𝑠 → ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) ↔ ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) ) )
79 oveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝑎 𝐹 𝑟 ) = ( 𝑎 𝐹 𝑠 ) )
80 79 eleq1d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ↔ ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) ) )
81 78 80 imbi12d ⊢ ( 𝑟 = 𝑠 → ( ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) ) ) )
82 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) )
83 nfcv ⊢ Ⅎ 𝑥 𝑎
84 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
85 7 84 nfcxfr ⊢ Ⅎ 𝑥 𝐹
86 nfcv ⊢ Ⅎ 𝑥 𝑟
87 83 85 86 nfov ⊢ Ⅎ 𝑥 ( 𝑎 𝐹 𝑟 )
88 87 nfel1 ⊢ Ⅎ 𝑥 ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 )
89 82 88 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) )
90 sseq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴 ) )
91 xpeq12 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑥 = 𝑎 ) → ( 𝑥 × 𝑥 ) = ( 𝑎 × 𝑎 ) )
92 91 anidms ⊢ ( 𝑥 = 𝑎 → ( 𝑥 × 𝑥 ) = ( 𝑎 × 𝑎 ) )
93 92 sseq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ) )
94 weeq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑟 We 𝑥 ↔ 𝑟 We 𝑎 ) )
95 90 93 94 3anbi123d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ↔ ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ) )
96 breq2 ⊢ ( 𝑥 = 𝑎 → ( ω ≼ 𝑥 ↔ ω ≼ 𝑎 ) )
97 95 96 anbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) )
98 4 97 syl5bb ⊢ ( 𝑥 = 𝑎 → ( 𝜓 ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) )
99 98 anbi2d ⊢ ( 𝑥 = 𝑎 → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) ) )
100 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 𝐹 𝑟 ) = ( 𝑎 𝐹 𝑟 ) )
101 difeq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑎 ) )
102 100 101 eleq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) ↔ ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ) )
103 99 102 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ) ) )
104 1 2 3 4 5 6 7 pwfseqlem3 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) )
105 89 103 104 chvarfv ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) )
106 73 81 105 chvarfv ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) )
107 106 eldifbd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ¬ ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 )
108 107 expr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ω ≼ 𝑎 → ¬ ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 ) )
109 65 108 sylbird ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ¬ 𝑎 ≺ ω → ¬ ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 ) )
110 109 con4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ( 𝑎 𝐹 𝑠 ) ∈ 𝑎 → 𝑎 ≺ ω ) )
111 48 56 110 vtocl ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑎 × 𝑎 ) ∧ ( 𝑊 ‘ 𝑍 ) We 𝑎 ) ) → ( ( 𝑎 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑎 → 𝑎 ≺ ω ) )
112 47 111 vtoclg ⊢ ( 𝑍 ∈ V → ( 𝜑 → ( ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 → 𝑍 ≺ ω ) ) )
113 29 112 mpcom ⊢ ( 𝜑 → ( ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) ∈ 𝑍 → 𝑍 ≺ ω ) )
114 23 113 mpd ⊢ ( 𝜑 → 𝑍 ≺ ω )
115 isfinite ⊢ ( 𝑍 ∈ Fin ↔ 𝑍 ≺ ω )
116 114 115 sylibr ⊢ ( 𝜑 → 𝑍 ∈ Fin )
117 1 2 3 4 5 6 7 pwfseqlem2 ⊢ ( ( 𝑍 ∈ Fin ∧ ( 𝑊 ‘ 𝑍 ) ∈ V ) → ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
118 116 48 117 sylancl ⊢ ( 𝜑 → ( 𝑍 𝐹 ( 𝑊 ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
119 118 23 eqeltrrd ⊢ ( 𝜑 → ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ 𝑍 )
120 8 19 24 fpwwe2lem3 ⊢ ( ( 𝜑 ∧ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ 𝑍 ) → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ) = ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
121 119 120 mpdan ⊢ ( 𝜑 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ) = ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
122 cnvimass ⊢ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊆ dom ( 𝑊 ‘ 𝑍 )
123 27 simprd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) )
124 dmss ⊢ ( ( 𝑊 ‘ 𝑍 ) ⊆ ( 𝑍 × 𝑍 ) → dom ( 𝑊 ‘ 𝑍 ) ⊆ dom ( 𝑍 × 𝑍 ) )
125 123 124 syl ⊢ ( 𝜑 → dom ( 𝑊 ‘ 𝑍 ) ⊆ dom ( 𝑍 × 𝑍 ) )
126 dmxpss ⊢ dom ( 𝑍 × 𝑍 ) ⊆ 𝑍
127 125 126 sstrdi ⊢ ( 𝜑 → dom ( 𝑊 ‘ 𝑍 ) ⊆ 𝑍 )
128 122 127 sstrid ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊆ 𝑍 )
129 116 128 ssfid ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ Fin )
130 48 inex1 ⊢ ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ∈ V
131 1 2 3 4 5 6 7 pwfseqlem2 ⊢ ( ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ Fin ∧ ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ∈ V ) → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
132 129 130 131 sylancl ⊢ ( 𝜑 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) × ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
133 121 132 eqtr3d ⊢ ( 𝜑 → ( 𝐻 ‘ ( card ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
134 f1of1 ⊢ ( 𝐻 : ω –1-1-onto→ 𝑋 → 𝐻 : ω –1-1→ 𝑋 )
135 3 134 syl ⊢ ( 𝜑 → 𝐻 : ω –1-1→ 𝑋 )
136 ficardom ⊢ ( 𝑍 ∈ Fin → ( card ‘ 𝑍 ) ∈ ω )
137 116 136 syl ⊢ ( 𝜑 → ( card ‘ 𝑍 ) ∈ ω )
138 ficardom ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ Fin → ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ∈ ω )
139 129 138 syl ⊢ ( 𝜑 → ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ∈ ω )
140 f1fveq ⊢ ( ( 𝐻 : ω –1-1→ 𝑋 ∧ ( ( card ‘ 𝑍 ) ∈ ω ∧ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ∈ ω ) ) → ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ↔ ( card ‘ 𝑍 ) = ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
141 135 137 139 140 syl12anc ⊢ ( 𝜑 → ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) = ( 𝐻 ‘ ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) ↔ ( card ‘ 𝑍 ) = ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) ) )
142 133 141 mpbid ⊢ ( 𝜑 → ( card ‘ 𝑍 ) = ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) )
143 142 eqcomd ⊢ ( 𝜑 → ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) = ( card ‘ 𝑍 ) )
144 finnum ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ Fin → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ dom card )
145 129 144 syl ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ dom card )
146 finnum ⊢ ( 𝑍 ∈ Fin → 𝑍 ∈ dom card )
147 116 146 syl ⊢ ( 𝜑 → 𝑍 ∈ dom card )
148 carden2 ⊢ ( ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ∈ dom card ∧ 𝑍 ∈ dom card ) → ( ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) = ( card ‘ 𝑍 ) ↔ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
149 145 147 148 syl2anc ⊢ ( 𝜑 → ( ( card ‘ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ) = ( card ‘ 𝑍 ) ↔ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
150 143 149 mpbid ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 )
151 dfpss2 ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ↔ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊆ 𝑍 ∧ ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 ) )
152 151 baib ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊆ 𝑍 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ↔ ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 ) )
153 128 152 syl ⊢ ( 𝜑 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ↔ ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 ) )
154 php3 ⊢ ( ( 𝑍 ∈ Fin ∧ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ) → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≺ 𝑍 )
155 sdomnen ⊢ ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≺ 𝑍 → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 )
156 154 155 syl ⊢ ( ( 𝑍 ∈ Fin ∧ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 ) → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 )
157 156 ex ⊢ ( 𝑍 ∈ Fin → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
158 116 157 syl ⊢ ( 𝜑 → ( ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ⊊ 𝑍 → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
159 153 158 sylbird ⊢ ( 𝜑 → ( ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 → ¬ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ≈ 𝑍 ) )
160 150 159 mt4d ⊢ ( 𝜑 → ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) = 𝑍 )
161 119 160 eleqtrrd ⊢ ( 𝜑 → ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) )
162 fvex ⊢ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ V
163 162 eliniseg ⊢ ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ V → ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ↔ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ) )
164 162 163 ax-mp ⊢ ( ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { ( 𝐻 ‘ ( card ‘ 𝑍 ) ) } ) ↔ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
165 161 164 sylib ⊢ ( 𝜑 → ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
166 26 simprd ⊢ ( 𝜑 → ( ( 𝑊 ‘ 𝑍 ) We 𝑍 ∧ ∀ 𝑏 ∈ 𝑍 [ ( ◡ ( 𝑊 ‘ 𝑍 ) “ { 𝑏 } ) / 𝑣 ] ( 𝑣 𝐹 ( ( 𝑊 ‘ 𝑍 ) ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑏 ) )
167 166 simpld ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑍 ) We 𝑍 )
168 weso ⊢ ( ( 𝑊 ‘ 𝑍 ) We 𝑍 → ( 𝑊 ‘ 𝑍 ) Or 𝑍 )
169 167 168 syl ⊢ ( 𝜑 → ( 𝑊 ‘ 𝑍 ) Or 𝑍 )
170 sonr ⊢ ( ( ( 𝑊 ‘ 𝑍 ) Or 𝑍 ∧ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ∈ 𝑍 ) → ¬ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
171 169 119 170 syl2anc ⊢ ( 𝜑 → ¬ ( 𝐻 ‘ ( card ‘ 𝑍 ) ) ( 𝑊 ‘ 𝑍 ) ( 𝐻 ‘ ( card ‘ 𝑍 ) ) )
172 165 171 pm2.65i ⊢ ¬ 𝜑