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 𝐾 ) ) )