Metamath Proof Explorer

Theorem axdclem

Description: Lemma for axdc . (Contributed by Mario Carneiro, 25-Jan-2013)

Ref Expression
Hypothesis axdclem.1 ⊢ 𝐹 = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω )
Assertion axdclem ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) → ( 𝐾 ∈ ω → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝐹 ‘ suc 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 axdclem.1 ⊢ 𝐹 = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω )
2 neeq1 ⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( 𝑦 ≠ ∅ ↔ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ≠ ∅ ) )
3 abn0 ⊢ ( { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ≠ ∅ ↔ ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 )
4 2 3 bitrdi ⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( 𝑦 ≠ ∅ ↔ ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) )
5 eleq2 ⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑔 ‘ 𝑦 ) ∈ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) )
6 breq2 ⊢ ( 𝑤 = 𝑧 → ( ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) )
7 6 cbvabv ⊢ { 𝑤 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 } = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 }
8 7 eleq2i ⊢ ( ( 𝑔 ‘ 𝑦 ) ∈ { 𝑤 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 } ↔ ( 𝑔 ‘ 𝑦 ) ∈ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } )
9 5 8 bitr4di ⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑔 ‘ 𝑦 ) ∈ { 𝑤 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 } ) )
10 fvex ⊢ ( 𝑔 ‘ 𝑦 ) ∈ V
11 breq2 ⊢ ( 𝑤 = ( 𝑔 ‘ 𝑦 ) → ( ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ 𝑦 ) ) )
12 10 11 elab ⊢ ( ( 𝑔 ‘ 𝑦 ) ∈ { 𝑤 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 } ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ 𝑦 ) )
13 9 12 bitrdi ⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ 𝑦 ) ) )
14 fveq2 ⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) )
15 14 breq2d ⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) )
16 13 15 bitrd ⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) )
17 4 16 imbi12d ⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ( ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) ) )
18 17 rspcv ⊢ ( { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ∈ 𝒫 dom 𝑥 → ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) ) )
19 fvex ⊢ ( 𝐹 ‘ 𝐾 ) ∈ V
20 vex ⊢ 𝑧 ∈ V
21 19 20 brelrn ⊢ ( ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 → 𝑧 ∈ ran 𝑥 )
22 21 abssi ⊢ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ ran 𝑥
23 sstr ⊢ ( ( { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ ran 𝑥 ∧ ran 𝑥 ⊆ dom 𝑥 ) → { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ dom 𝑥 )
24 22 23 mpan ⊢ ( ran 𝑥 ⊆ dom 𝑥 → { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ dom 𝑥 )
25 vex ⊢ 𝑥 ∈ V
26 25 dmex ⊢ dom 𝑥 ∈ V
27 26 elpw2 ⊢ ( { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ∈ 𝒫 dom 𝑥 ↔ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ dom 𝑥 )
28 24 27 sylibr ⊢ ( ran 𝑥 ⊆ dom 𝑥 → { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ∈ 𝒫 dom 𝑥 )
29 18 28 syl11 ⊢ ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( ran 𝑥 ⊆ dom 𝑥 → ( ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) ) )
30 29 3imp ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) )
31 fvex ⊢ ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ∈ V
32 nfcv ⊢ Ⅎ 𝑦 𝑠
33 nfcv ⊢ Ⅎ 𝑦 𝐾
34 nfcv ⊢ Ⅎ 𝑦 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } )
35 breq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐾 ) → ( 𝑦 𝑥 𝑧 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) )
36 35 abbidv ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐾 ) → { 𝑧 ∣ 𝑦 𝑥 𝑧 } = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } )
37 36 fveq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐾 ) → ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) = ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) )
38 32 33 34 1 37 frsucmpt ⊢ ( ( 𝐾 ∈ ω ∧ ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ∈ V ) → ( 𝐹 ‘ suc 𝐾 ) = ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) )
39 31 38 mpan2 ⊢ ( 𝐾 ∈ ω → ( 𝐹 ‘ suc 𝐾 ) = ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) )
40 39 breq2d ⊢ ( 𝐾 ∈ ω → ( ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝐹 ‘ suc 𝐾 ) ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) )
41 30 40 syl5ibrcom ⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) → ( 𝐾 ∈ ω → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝐹 ‘ suc 𝐾 ) ) )