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

Metamath Proof Explorer

Theorem aomclem7

Description: Lemma for dfac11 . ( R1A ) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem6.b ⊢ B = a b | ∃ c ∈ R1 ⁡ ⋃ dom ⁡ z c ∈ b ∧ ¬ c ∈ a ∧ ∀ d ∈ R1 ⁡ ⋃ dom ⁡ z d z ⁡ ⋃ dom ⁡ z c → d ∈ a ↔ d ∈ b
aomclem6.c ⊢ C = a ∈ V ⟼ sup y ⁡ a R1 ⁡ dom ⁡ z B
aomclem6.d ⊢ D = recs ⁡ a ∈ V ⟼ C ⁡ R1 ⁡ dom ⁡ z ∖ ran ⁡ a
aomclem6.e ⊢ E = a b | ⋂ D -1 a ∈ ⋂ D -1 b
aomclem6.f ⊢ F = a b | rank ⁡ a E rank ⁡ b ∨ rank ⁡ a = rank ⁡ b ∧ a z ⁡ suc ⁡ rank ⁡ a b
aomclem6.g ⊢ G = if dom ⁡ z = ⋃ dom ⁡ z F E ∩ R1 ⁡ dom ⁡ z × R1 ⁡ dom ⁡ z
aomclem6.h ⊢ H = recs ⁡ z ∈ V ⟼ G
aomclem6.a ⊢ φ → A ∈ On
aomclem6.y ⊢ φ → ∀ a ∈ 𝒫 R1 ⁡ A a ≠ ∅ → y ⁡ a ∈ 𝒫 a ∩ Fin ∖ ∅
Assertion aomclem7 ⊢ φ → ∃ b b We R1 ⁡ A

Proof

Step Hyp Ref Expression
1 aomclem6.b ⊢ B = a b | ∃ c ∈ R1 ⁡ ⋃ dom ⁡ z c ∈ b ∧ ¬ c ∈ a ∧ ∀ d ∈ R1 ⁡ ⋃ dom ⁡ z d z ⁡ ⋃ dom ⁡ z c → d ∈ a ↔ d ∈ b
2 aomclem6.c ⊢ C = a ∈ V ⟼ sup y ⁡ a R1 ⁡ dom ⁡ z B
3 aomclem6.d ⊢ D = recs ⁡ a ∈ V ⟼ C ⁡ R1 ⁡ dom ⁡ z ∖ ran ⁡ a
4 aomclem6.e ⊢ E = a b | ⋂ D -1 a ∈ ⋂ D -1 b
5 aomclem6.f ⊢ F = a b | rank ⁡ a E rank ⁡ b ∨ rank ⁡ a = rank ⁡ b ∧ a z ⁡ suc ⁡ rank ⁡ a b
6 aomclem6.g ⊢ G = if dom ⁡ z = ⋃ dom ⁡ z F E ∩ R1 ⁡ dom ⁡ z × R1 ⁡ dom ⁡ z
7 aomclem6.h ⊢ H = recs ⁡ z ∈ V ⟼ G
8 aomclem6.a ⊢ φ → A ∈ On
9 aomclem6.y ⊢ φ → ∀ a ∈ 𝒫 R1 ⁡ A a ≠ ∅ → y ⁡ a ∈ 𝒫 a ∩ Fin ∖ ∅
10 1 2 3 4 5 6 7 8 9 aomclem6 ⊢ φ → H ⁡ A We R1 ⁡ A
11 fvex ⊢ H ⁡ A ∈ V
12 weeq1 ⊢ b = H ⁡ A → b We R1 ⁡ A ↔ H ⁡ A We R1 ⁡ A
13 11 12 spcev ⊢ H ⁡ A We R1 ⁡ A → ∃ b b We R1 ⁡ A
14 10 13 syl ⊢ φ → ∃ b b We R1 ⁡ A