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 ffvelrnd ( ( 𝜑𝜓 ) → ( 𝐺 ‘ { 𝑤𝑥 ∣ ( ( 𝐾𝑤 ) ∈ 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 ffvelrn ( ( 𝐾 : 𝑛 ∈ ω ( 𝑥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 𝑛 ) ) )