Metamath Proof Explorer

Theorem axdclem

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

Ref Expression
Hypothesis axdclem.1 ⊢ F = rec ⁡ y ∈ V ⟼ g ⁡ z | y x z s ↾ ω
Assertion axdclem ⊢ ∀ y ∈ 𝒫 dom ⁡ x y ≠ ∅ → g ⁡ y ∈ y ∧ ran ⁡ x ⊆ dom ⁡ x ∧ ∃ z F ⁡ K x z → K ∈ ω → F ⁡ K x F ⁡ suc ⁡ K

Proof

Step Hyp Ref Expression
1 axdclem.1 ⊢ F = rec ⁡ y ∈ V ⟼ g ⁡ z | y x z s ↾ ω
2 neeq1 ⊢ y = z | F ⁡ K x z → y ≠ ∅ ↔ z | F ⁡ K x z ≠ ∅
3 abn0 ⊢ z | F ⁡ K x z ≠ ∅ ↔ ∃ z F ⁡ K x z
4 2 3 bitrdi ⊢ y = z | F ⁡ K x z → y ≠ ∅ ↔ ∃ z F ⁡ K x z
5 eleq2 ⊢ y = z | F ⁡ K x z → g ⁡ y ∈ y ↔ g ⁡ y ∈ z | F ⁡ K x z
6 breq2 ⊢ w = z → F ⁡ K x w ↔ F ⁡ K x z
7 6 cbvabv ⊢ w | F ⁡ K x w = z | F ⁡ K x z
8 7 eleq2i ⊢ g ⁡ y ∈ w | F ⁡ K x w ↔ g ⁡ y ∈ z | F ⁡ K x z
9 5 8 bitr4di ⊢ y = z | F ⁡ K x z → g ⁡ y ∈ y ↔ g ⁡ y ∈ w | F ⁡ K x w
10 fvex ⊢ g ⁡ y ∈ V
11 breq2 ⊢ w = g ⁡ y → F ⁡ K x w ↔ F ⁡ K x g ⁡ y
12 10 11 elab ⊢ g ⁡ y ∈ w | F ⁡ K x w ↔ F ⁡ K x g ⁡ y
13 9 12 bitrdi ⊢ y = z | F ⁡ K x z → g ⁡ y ∈ y ↔ F ⁡ K x g ⁡ y
14 fveq2 ⊢ y = z | F ⁡ K x z → g ⁡ y = g ⁡ z | F ⁡ K x z
15 14 breq2d ⊢ y = z | F ⁡ K x z → F ⁡ K x g ⁡ y ↔ F ⁡ K x g ⁡ z | F ⁡ K x z
16 13 15 bitrd ⊢ y = z | F ⁡ K x z → g ⁡ y ∈ y ↔ F ⁡ K x g ⁡ z | F ⁡ K x z
17 4 16 imbi12d ⊢ y = z | F ⁡ K x z → y ≠ ∅ → g ⁡ y ∈ y ↔ ∃ z F ⁡ K x z → F ⁡ K x g ⁡ z | F ⁡ K x z
18 17 rspcv ⊢ z | F ⁡ K x z ∈ 𝒫 dom ⁡ x → ∀ y ∈ 𝒫 dom ⁡ x y ≠ ∅ → g ⁡ y ∈ y → ∃ z F ⁡ K x z → F ⁡ K x g ⁡ z | F ⁡ K x z
19 fvex ⊢ F ⁡ K ∈ V
20 vex ⊢ z ∈ V
21 19 20 brelrn ⊢ F ⁡ K x z → z ∈ ran ⁡ x
22 21 abssi ⊢ z | F ⁡ K x z ⊆ ran ⁡ x
23 sstr ⊢ z | F ⁡ K x z ⊆ ran ⁡ x ∧ ran ⁡ x ⊆ dom ⁡ x → z | F ⁡ K x z ⊆ dom ⁡ x
24 22 23 mpan ⊢ ran ⁡ x ⊆ dom ⁡ x → z | F ⁡ K x z ⊆ dom ⁡ x
25 vex ⊢ x ∈ V
26 25 dmex ⊢ dom ⁡ x ∈ V
27 26 elpw2 ⊢ z | F ⁡ K x z ∈ 𝒫 dom ⁡ x ↔ z | F ⁡ K x z ⊆ dom ⁡ x
28 24 27 sylibr ⊢ ran ⁡ x ⊆ dom ⁡ x → z | F ⁡ K x z ∈ 𝒫 dom ⁡ x
29 18 28 syl11 ⊢ ∀ y ∈ 𝒫 dom ⁡ x y ≠ ∅ → g ⁡ y ∈ y → ran ⁡ x ⊆ dom ⁡ x → ∃ z F ⁡ K x z → F ⁡ K x g ⁡ z | F ⁡ K x z
30 29 3imp ⊢ ∀ y ∈ 𝒫 dom ⁡ x y ≠ ∅ → g ⁡ y ∈ y ∧ ran ⁡ x ⊆ dom ⁡ x ∧ ∃ z F ⁡ K x z → F ⁡ K x g ⁡ z | F ⁡ K x z
31 fvex ⊢ g ⁡ z | F ⁡ K x z ∈ V
32 nfcv ⊢ Ⅎ _ y s
33 nfcv ⊢ Ⅎ _ y K
34 nfcv ⊢ Ⅎ _ y g ⁡ z | F ⁡ K x z
35 breq1 ⊢ y = F ⁡ K → y x z ↔ F ⁡ K x z
36 35 abbidv ⊢ y = F ⁡ K → z | y x z = z | F ⁡ K x z
37 36 fveq2d ⊢ y = F ⁡ K → g ⁡ z | y x z = g ⁡ z | F ⁡ K x z
38 32 33 34 1 37 frsucmpt ⊢ K ∈ ω ∧ g ⁡ z | F ⁡ K x z ∈ V → F ⁡ suc ⁡ K = g ⁡ z | F ⁡ K x z
39 31 38 mpan2 ⊢ K ∈ ω → F ⁡ suc ⁡ K = g ⁡ z | F ⁡ K x z
40 39 breq2d ⊢ K ∈ ω → F ⁡ K x F ⁡ suc ⁡ K ↔ F ⁡ K x g ⁡ z | F ⁡ K x z
41 30 40 syl5ibrcom ⊢ ∀ y ∈ 𝒫 dom ⁡ x y ≠ ∅ → g ⁡ y ∈ y ∧ ran ⁡ x ⊆ dom ⁡ x ∧ ∃ z F ⁡ K x z → K ∈ ω → F ⁡ K x F ⁡ suc ⁡ K