This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwfseqlem3

Description: Lemma for pwfseq . Using the construction D from pwfseqlem1 , produce a function F that maps any well-ordered infinite set to an element outside the set. (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 ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
Assertion pwfseqlem3 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) )

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 vex ⊢ 𝑥 ∈ V
9 vex ⊢ 𝑟 ∈ V
10 fvex ⊢ ( 𝐻 ‘ ( card ‘ 𝑥 ) ) ∈ V
11 fvex ⊢ ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ V
12 10 11 ifex ⊢ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) ∈ V
13 7 ovmpt4g ⊢ ( ( 𝑥 ∈ V ∧ 𝑟 ∈ V ∧ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) ∈ V ) → ( 𝑥 𝐹 𝑟 ) = if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
14 8 9 12 13 mp3an ⊢ ( 𝑥 𝐹 𝑟 ) = if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) )
15 4 simprbi ⊢ ( 𝜓 → ω ≼ 𝑥 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ω ≼ 𝑥 )
17 domnsym ⊢ ( ω ≼ 𝑥 → ¬ 𝑥 ≺ ω )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ 𝑥 ≺ ω )
19 isfinite ⊢ ( 𝑥 ∈ Fin ↔ 𝑥 ≺ ω )
20 18 19 sylnibr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ 𝑥 ∈ Fin )
21 20 iffalsed ⊢ ( ( 𝜑 ∧ 𝜓 ) → if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) = ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) )
22 14 21 eqtrid ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑟 ) = ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) )
23 1 2 3 4 5 6 pwfseqlem1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∖ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) )
24 eldif ⊢ ( 𝐷 ∈ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∖ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) ↔ ( 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ ¬ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) )
25 23 24 sylib ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ ¬ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) ) )
26 25 simpld ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
27 eliun ⊢ ( 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↔ ∃ 𝑛 ∈ ω 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) )
28 26 27 sylib ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑛 ∈ ω 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) )
29 elmapi ⊢ ( 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) → 𝐷 : 𝑛 ⟶ 𝐴 )
30 29 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → 𝐷 : 𝑛 ⟶ 𝐴 )
31 ssiun2 ⊢ ( 𝑛 ∈ ω → ( 𝑥 ↑m 𝑛 ) ⊆ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) )
32 31 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( 𝑥 ↑m 𝑛 ) ⊆ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) )
33 25 simprd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ¬ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) )
35 32 34 ssneldd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ¬ 𝐷 ∈ ( 𝑥 ↑m 𝑛 ) )
36 vex ⊢ 𝑛 ∈ V
37 8 36 elmap ⊢ ( 𝐷 ∈ ( 𝑥 ↑m 𝑛 ) ↔ 𝐷 : 𝑛 ⟶ 𝑥 )
38 ffn ⊢ ( 𝐷 : 𝑛 ⟶ 𝐴 → 𝐷 Fn 𝑛 )
39 ffnfv ⊢ ( 𝐷 : 𝑛 ⟶ 𝑥 ↔ ( 𝐷 Fn 𝑛 ∧ ∀ 𝑧 ∈ 𝑛 ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
40 39 baib ⊢ ( 𝐷 Fn 𝑛 → ( 𝐷 : 𝑛 ⟶ 𝑥 ↔ ∀ 𝑧 ∈ 𝑛 ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
41 30 38 40 3syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( 𝐷 : 𝑛 ⟶ 𝑥 ↔ ∀ 𝑧 ∈ 𝑛 ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
42 37 41 bitrid ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( 𝐷 ∈ ( 𝑥 ↑m 𝑛 ) ↔ ∀ 𝑧 ∈ 𝑛 ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
43 35 42 mtbid ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ¬ ∀ 𝑧 ∈ 𝑛 ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 )
44 nnon ⊢ ( 𝑛 ∈ ω → 𝑛 ∈ On )
45 44 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → 𝑛 ∈ On )
46 ssrab2 ⊢ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ⊆ ω
47 omsson ⊢ ω ⊆ On
48 46 47 sstri ⊢ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ⊆ On
49 ordom ⊢ Ord ω
50 simprl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → 𝑛 ∈ ω )
51 ordelss ⊢ ( ( Ord ω ∧ 𝑛 ∈ ω ) → 𝑛 ⊆ ω )
52 49 50 51 sylancr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → 𝑛 ⊆ ω )
53 rexnal ⊢ ( ∃ 𝑧 ∈ 𝑛 ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ↔ ¬ ∀ 𝑧 ∈ 𝑛 ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 )
54 43 53 sylibr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ∃ 𝑧 ∈ 𝑛 ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 )
55 ssrexv ⊢ ( 𝑛 ⊆ ω → ( ∃ 𝑧 ∈ 𝑛 ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → ∃ 𝑧 ∈ ω ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
56 52 54 55 sylc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ∃ 𝑧 ∈ ω ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 )
57 rabn0 ⊢ ( { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ≠ ∅ ↔ ∃ 𝑧 ∈ ω ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 )
58 56 57 sylibr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ≠ ∅ )
59 onint ⊢ ( ( { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ⊆ On ∧ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ≠ ∅ ) → ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } )
60 48 58 59 sylancr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } )
61 48 60 sselid ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ On )
62 ontri1 ⊢ ( ( 𝑛 ∈ On ∧ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ On ) → ( 𝑛 ⊆ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ↔ ¬ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ 𝑛 ) )
63 45 61 62 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( 𝑛 ⊆ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ↔ ¬ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ 𝑛 ) )
64 ssintrab ⊢ ( 𝑛 ⊆ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ↔ ∀ 𝑧 ∈ ω ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → 𝑛 ⊆ 𝑧 ) )
65 nnon ⊢ ( 𝑧 ∈ ω → 𝑧 ∈ On )
66 ontri1 ⊢ ( ( 𝑛 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑛 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑛 ) )
67 44 65 66 syl2an ⊢ ( ( 𝑛 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑛 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑛 ) )
68 67 imbi2d ⊢ ( ( 𝑛 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → 𝑛 ⊆ 𝑧 ) ↔ ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → ¬ 𝑧 ∈ 𝑛 ) ) )
69 con34b ⊢ ( ( 𝑧 ∈ 𝑛 → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ↔ ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → ¬ 𝑧 ∈ 𝑛 ) )
70 68 69 bitr4di ⊢ ( ( 𝑛 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → 𝑛 ⊆ 𝑧 ) ↔ ( 𝑧 ∈ 𝑛 → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) )
71 70 pm5.74da ⊢ ( 𝑛 ∈ ω → ( ( 𝑧 ∈ ω → ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → 𝑛 ⊆ 𝑧 ) ) ↔ ( 𝑧 ∈ ω → ( 𝑧 ∈ 𝑛 → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) ) )
72 bi2.04 ⊢ ( ( 𝑧 ∈ ω → ( 𝑧 ∈ 𝑛 → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑛 → ( 𝑧 ∈ ω → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) )
73 71 72 bitrdi ⊢ ( 𝑛 ∈ ω → ( ( 𝑧 ∈ ω → ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → 𝑛 ⊆ 𝑧 ) ) ↔ ( 𝑧 ∈ 𝑛 → ( 𝑧 ∈ ω → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) ) )
74 elnn ⊢ ( ( 𝑧 ∈ 𝑛 ∧ 𝑛 ∈ ω ) → 𝑧 ∈ ω )
75 pm2.27 ⊢ ( 𝑧 ∈ ω → ( ( 𝑧 ∈ ω → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
76 74 75 syl ⊢ ( ( 𝑧 ∈ 𝑛 ∧ 𝑛 ∈ ω ) → ( ( 𝑧 ∈ ω → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
77 76 expcom ⊢ ( 𝑛 ∈ ω → ( 𝑧 ∈ 𝑛 → ( ( 𝑧 ∈ ω → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) )
78 77 a2d ⊢ ( 𝑛 ∈ ω → ( ( 𝑧 ∈ 𝑛 → ( 𝑧 ∈ ω → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) → ( 𝑧 ∈ 𝑛 → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) )
79 73 78 sylbid ⊢ ( 𝑛 ∈ ω → ( ( 𝑧 ∈ ω → ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → 𝑛 ⊆ 𝑧 ) ) → ( 𝑧 ∈ 𝑛 → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) )
80 79 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( ( 𝑧 ∈ ω → ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → 𝑛 ⊆ 𝑧 ) ) → ( 𝑧 ∈ 𝑛 → ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) ) )
81 80 ralimdv2 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( ∀ 𝑧 ∈ ω ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 → 𝑛 ⊆ 𝑧 ) → ∀ 𝑧 ∈ 𝑛 ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
82 64 81 biimtrid ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( 𝑛 ⊆ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } → ∀ 𝑧 ∈ 𝑛 ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
83 63 82 sylbird ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( ¬ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ 𝑛 → ∀ 𝑧 ∈ 𝑛 ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ) )
84 43 83 mt3d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ 𝑛 )
85 30 84 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ 𝐴 )
86 fveq2 ⊢ ( 𝑦 = ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } → ( 𝐷 ‘ 𝑦 ) = ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) )
87 86 eleq1d ⊢ ( 𝑦 = ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } → ( ( 𝐷 ‘ 𝑦 ) ∈ 𝑥 ↔ ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ 𝑥 ) )
88 87 notbid ⊢ ( 𝑦 = ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } → ( ¬ ( 𝐷 ‘ 𝑦 ) ∈ 𝑥 ↔ ¬ ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ 𝑥 ) )
89 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐷 ‘ 𝑧 ) = ( 𝐷 ‘ 𝑦 ) )
90 89 eleq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ↔ ( 𝐷 ‘ 𝑦 ) ∈ 𝑥 ) )
91 90 notbid ⊢ ( 𝑧 = 𝑦 → ( ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 ↔ ¬ ( 𝐷 ‘ 𝑦 ) ∈ 𝑥 ) )
92 91 cbvrabv ⊢ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } = { 𝑦 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑦 ) ∈ 𝑥 }
93 88 92 elrab2 ⊢ ( ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ↔ ( ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ ω ∧ ¬ ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ 𝑥 ) )
94 93 simprbi ⊢ ( ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ∈ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } → ¬ ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ 𝑥 )
95 60 94 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ¬ ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ 𝑥 )
96 85 95 eldifd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑛 ∈ ω ∧ 𝐷 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ ( 𝐴 ∖ 𝑥 ) )
97 28 96 rexlimddv ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ ( 𝐴 ∖ 𝑥 ) )
98 22 97 eqeltrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) )