Metamath Proof Explorer

Theorem pwfseqlem4a

Description: Lemma for pwfseqlem4 . (Contributed by Mario Carneiro, 7-Jun-2016)

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 pwfseqlem4a ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 )

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 isfinite ⊢ ( 𝑎 ∈ Fin ↔ 𝑎 ≺ ω )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ Fin ) → 𝑎 ∈ Fin )
10 vex ⊢ 𝑠 ∈ V
11 1 2 3 4 5 6 7 pwfseqlem2 ⊢ ( ( 𝑎 ∈ Fin ∧ 𝑠 ∈ V ) → ( 𝑎 𝐹 𝑠 ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) ) )
12 9 10 11 sylancl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ Fin ) → ( 𝑎 𝐹 𝑠 ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) ) )
13 f1of ⊢ ( 𝐻 : ω –1-1-onto→ 𝑋 → 𝐻 : ω ⟶ 𝑋 )
14 3 13 syl ⊢ ( 𝜑 → 𝐻 : ω ⟶ 𝑋 )
15 14 2 fssd ⊢ ( 𝜑 → 𝐻 : ω ⟶ 𝐴 )
16 ficardom ⊢ ( 𝑎 ∈ Fin → ( card ‘ 𝑎 ) ∈ ω )
17 ffvelcdm ⊢ ( ( 𝐻 : ω ⟶ 𝐴 ∧ ( card ‘ 𝑎 ) ∈ ω ) → ( 𝐻 ‘ ( card ‘ 𝑎 ) ) ∈ 𝐴 )
18 15 16 17 syl2an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ Fin ) → ( 𝐻 ‘ ( card ‘ 𝑎 ) ) ∈ 𝐴 )
19 12 18 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ Fin ) → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 )
20 19 ex ⊢ ( 𝜑 → ( 𝑎 ∈ Fin → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( 𝑎 ∈ Fin → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 ) )
22 8 21 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( 𝑎 ≺ ω → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 ) )
23 omelon ⊢ ω ∈ On
24 onenon ⊢ ( ω ∈ On → ω ∈ dom card )
25 23 24 ax-mp ⊢ ω ∈ dom card
26 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → 𝑠 We 𝑎 )
27 26 19.8ad ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ∃ 𝑠 𝑠 We 𝑎 )
28 ween ⊢ ( 𝑎 ∈ dom card ↔ ∃ 𝑠 𝑠 We 𝑎 )
29 27 28 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → 𝑎 ∈ dom card )
30 domtri2 ⊢ ( ( ω ∈ dom card ∧ 𝑎 ∈ dom card ) → ( ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω ) )
31 25 29 30 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω ) )
32 nfv ⊢ Ⅎ 𝑟 ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) )
33 nfcv ⊢ Ⅎ 𝑟 𝑎
34 nfmpo2 ⊢ Ⅎ 𝑟 ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
35 7 34 nfcxfr ⊢ Ⅎ 𝑟 𝐹
36 nfcv ⊢ Ⅎ 𝑟 𝑠
37 33 35 36 nfov ⊢ Ⅎ 𝑟 ( 𝑎 𝐹 𝑠 )
38 37 nfel1 ⊢ Ⅎ 𝑟 ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 )
39 32 38 nfim ⊢ Ⅎ 𝑟 ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) )
40 sseq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 ⊆ ( 𝑎 × 𝑎 ) ↔ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) )
41 weeq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 We 𝑎 ↔ 𝑠 We 𝑎 ) )
42 40 41 3anbi23d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ↔ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) )
43 42 anbi1d ⊢ ( 𝑟 = 𝑠 → ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) )
44 43 anbi2d ⊢ ( 𝑟 = 𝑠 → ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) ↔ ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) ) )
45 oveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝑎 𝐹 𝑟 ) = ( 𝑎 𝐹 𝑠 ) )
46 45 eleq1d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ↔ ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) ) )
47 44 46 imbi12d ⊢ ( 𝑟 = 𝑠 → ( ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) ) ) )
48 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) )
49 nfcv ⊢ Ⅎ 𝑥 𝑎
50 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
51 7 50 nfcxfr ⊢ Ⅎ 𝑥 𝐹
52 nfcv ⊢ Ⅎ 𝑥 𝑟
53 49 51 52 nfov ⊢ Ⅎ 𝑥 ( 𝑎 𝐹 𝑟 )
54 53 nfel1 ⊢ Ⅎ 𝑥 ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 )
55 48 54 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) )
56 sseq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴 ) )
57 xpeq12 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑥 = 𝑎 ) → ( 𝑥 × 𝑥 ) = ( 𝑎 × 𝑎 ) )
58 57 anidms ⊢ ( 𝑥 = 𝑎 → ( 𝑥 × 𝑥 ) = ( 𝑎 × 𝑎 ) )
59 58 sseq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ) )
60 weeq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑟 We 𝑥 ↔ 𝑟 We 𝑎 ) )
61 56 59 60 3anbi123d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ↔ ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ) )
62 breq2 ⊢ ( 𝑥 = 𝑎 → ( ω ≼ 𝑥 ↔ ω ≼ 𝑎 ) )
63 61 62 anbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) )
64 4 63 bitrid ⊢ ( 𝑥 = 𝑎 → ( 𝜓 ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) )
65 64 anbi2d ⊢ ( 𝑥 = 𝑎 → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) ) )
66 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 𝐹 𝑟 ) = ( 𝑎 𝐹 𝑟 ) )
67 difeq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑎 ) )
68 66 67 eleq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) ↔ ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ) )
69 65 68 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) ) ) )
70 1 2 3 4 5 6 7 pwfseqlem3 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑥 ) )
71 55 69 70 chvarfv ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑟 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑟 ) ∈ ( 𝐴 ∖ 𝑎 ) )
72 39 47 71 chvarfv ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ ( 𝐴 ∖ 𝑎 ) )
73 72 eldifad ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ∧ ω ≼ 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 )
74 73 expr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ω ≼ 𝑎 → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 ) )
75 31 74 sylbird ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( ¬ 𝑎 ≺ ω → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 ) )
76 22 75 pm2.61d ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ∧ 𝑠 We 𝑎 ) ) → ( 𝑎 𝐹 𝑠 ) ∈ 𝐴 )