Metamath Proof Explorer

Theorem pwfseqlem1

Description: Lemma for pwfseq . Derive a contradiction by diagonalization. (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 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } )
Assertion pwfseqlem1 ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∖ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) )

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 1 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
8 f1f ⊢ ( 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → 𝐺 : 𝒫 𝐴 ⟶ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
9 7 8 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : 𝒫 𝐴 ⟶ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
10 ssrab2 ⊢ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ⊆ 𝑥
11 simprl1 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) ) → 𝑥 ⊆ 𝐴 )
12 4 11 sylan2b ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ⊆ 𝐴 )
13 10 12 sstrid ⊢ ( ( 𝜑 ∧ 𝜓 ) → { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ⊆ 𝐴 )
14 vex ⊢ 𝑥 ∈ V
15 14 rabex ⊢ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ V
16 15 elpw ⊢ ( { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ 𝒫 𝐴 ↔ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ⊆ 𝐴 )
17 13 16 sylibr ⊢ ( ( 𝜑 ∧ 𝜓 ) → { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ 𝒫 𝐴 )
18 9 17 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
19 6 18 eqeltrid ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
20 pm5.19 ⊢ ¬ ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } )
21 5 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) –1-1→ 𝑥 )
22 f1f ⊢ ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) –1-1→ 𝑥 → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ⟶ 𝑥 )
23 21 22 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ⟶ 𝑥 )
24 ffvelcdm ⊢ ( ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ⟶ 𝑥 ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 )
25 23 24 sylancom ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 )
26 f1f1orn ⊢ ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) –1-1→ 𝑥 → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) –1-1-onto→ ran 𝐾 )
27 21 26 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) –1-1-onto→ ran 𝐾 )
28 f1ocnvfv1 ⊢ ( ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) –1-1-onto→ ran 𝐾 ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) = 𝐷 )
29 27 28 sylancom ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) = 𝐷 )
30 f1fn ⊢ ( 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → 𝐺 Fn 𝒫 𝐴 )
31 7 30 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 Fn 𝒫 𝐴 )
32 fnfvelrn ⊢ ( ( 𝐺 Fn 𝒫 𝐴 ∧ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ 𝒫 𝐴 ) → ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) ∈ ran 𝐺 )
33 31 17 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) ∈ ran 𝐺 )
34 6 33 eqeltrid ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ran 𝐺 )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → 𝐷 ∈ ran 𝐺 )
36 29 35 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 )
37 fveq2 ⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ◡ 𝐾 ‘ 𝑦 ) = ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) )
38 37 eleq1d ⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ( ◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ↔ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ) )
39 id ⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → 𝑦 = ( 𝐾 ‘ 𝐷 ) )
40 2fveq3 ⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑦 ) ) = ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) )
41 39 40 eleq12d ⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( 𝑦 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑦 ) ) ↔ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
42 41 notbid ⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ¬ 𝑦 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑦 ) ) ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
43 38 42 anbi12d ⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ( ( ◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ∧ ¬ 𝑦 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑦 ) ) ) ↔ ( ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) ) )
44 fveq2 ⊢ ( 𝑤 = 𝑦 → ( ◡ 𝐾 ‘ 𝑤 ) = ( ◡ 𝐾 ‘ 𝑦 ) )
45 44 eleq1d ⊢ ( 𝑤 = 𝑦 → ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ↔ ( ◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ) )
46 id ⊢ ( 𝑤 = 𝑦 → 𝑤 = 𝑦 )
47 2fveq3 ⊢ ( 𝑤 = 𝑦 → ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) = ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑦 ) ) )
48 46 47 eleq12d ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ↔ 𝑦 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑦 ) ) ) )
49 48 notbid ⊢ ( 𝑤 = 𝑦 → ( ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ↔ ¬ 𝑦 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑦 ) ) ) )
50 45 49 anbi12d ⊢ ( 𝑤 = 𝑦 → ( ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) ↔ ( ( ◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ∧ ¬ 𝑦 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑦 ) ) ) ) )
51 50 cbvrabv ⊢ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } = { 𝑦 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ∧ ¬ 𝑦 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑦 ) ) ) }
52 43 51 elrab2 ⊢ ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) ) )
53 anass ⊢ ( ( ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ) ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) ↔ ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) ) )
54 52 53 bitr4i ⊢ ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ( ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ) ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
55 54 baib ⊢ ( ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ) → ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
56 25 36 55 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
57 29 6 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) = ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) )
58 57 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) = ( ◡ 𝐺 ‘ ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) )
59 f1f1orn ⊢ ( 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → 𝐺 : 𝒫 𝐴 –1-1-onto→ ran 𝐺 )
60 7 59 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : 𝒫 𝐴 –1-1-onto→ ran 𝐺 )
61 f1ocnvfv1 ⊢ ( ( 𝐺 : 𝒫 𝐴 –1-1-onto→ ran 𝐺 ∧ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ 𝒫 𝐴 ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) = { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } )
62 60 17 61 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) = { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) = { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } )
64 58 63 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) = { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } )
65 64 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ↔ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) )
66 65 notbid ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) )
67 56 66 bitrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) → ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) )
68 67 ex ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) → ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) )
69 20 68 mtoi ⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) )
70 19 69 eldifd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∖ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) )