Metamath Proof Explorer

Theorem aomclem3

Description: Lemma for dfac11 . Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses aomclem3.b ⊢B=ab|∃c∈R1⁡⋃dom⁡zc∈b∧¬c∈a∧∀d∈R1⁡⋃dom⁡zdz⁡⋃dom⁡zc→d∈a↔d∈b
aomclem3.c ⊢C=a∈V⟼supy⁡aR1⁡dom⁡zB
aomclem3.d ⊢D=recs⁡a∈V⟼C⁡R1⁡dom⁡z∖ran⁡a
aomclem3.e ⊢E=ab|⋂D-1a∈⋂D-1b
aomclem3.on ⊢φ→dom⁡z∈On
aomclem3.su ⊢φ→dom⁡z=suc⁡⋃dom⁡z
aomclem3.we ⊢φ→∀a∈dom⁡zz⁡aWeR1⁡a
aomclem3.a ⊢φ→A∈On
aomclem3.za ⊢φ→dom⁡z⊆A
aomclem3.y ⊢φ→∀a∈𝒫R1⁡Aa≠∅→y⁡a∈𝒫a∩Fin∖∅
Assertion aomclem3 ⊢φ→EWeR1⁡dom⁡z

Proof

Step Hyp Ref Expression
1 aomclem3.b ⊢B=ab|∃c∈R1⁡⋃dom⁡zc∈b∧¬c∈a∧∀d∈R1⁡⋃dom⁡zdz⁡⋃dom⁡zc→d∈a↔d∈b
2 aomclem3.c ⊢C=a∈V⟼supy⁡aR1⁡dom⁡zB
3 aomclem3.d ⊢D=recs⁡a∈V⟼C⁡R1⁡dom⁡z∖ran⁡a
4 aomclem3.e ⊢E=ab|⋂D-1a∈⋂D-1b
5 aomclem3.on ⊢φ→dom⁡z∈On
6 aomclem3.su ⊢φ→dom⁡z=suc⁡⋃dom⁡z
7 aomclem3.we ⊢φ→∀a∈dom⁡zz⁡aWeR1⁡a
8 aomclem3.a ⊢φ→A∈On
9 aomclem3.za ⊢φ→dom⁡z⊆A
10 aomclem3.y ⊢φ→∀a∈𝒫R1⁡Aa≠∅→y⁡a∈𝒫a∩Fin∖∅
11 rneq ⊢a=c→ran⁡a=ran⁡c
12 11 difeq2d ⊢a=c→R1⁡dom⁡z∖ran⁡a=R1⁡dom⁡z∖ran⁡c
13 12 fveq2d ⊢a=c→C⁡R1⁡dom⁡z∖ran⁡a=C⁡R1⁡dom⁡z∖ran⁡c
14 13 cbvmptv ⊢a∈V⟼C⁡R1⁡dom⁡z∖ran⁡a=c∈V⟼C⁡R1⁡dom⁡z∖ran⁡c
15 recseq ⊢a∈V⟼C⁡R1⁡dom⁡z∖ran⁡a=c∈V⟼C⁡R1⁡dom⁡z∖ran⁡c→recs⁡a∈V⟼C⁡R1⁡dom⁡z∖ran⁡a=recs⁡c∈V⟼C⁡R1⁡dom⁡z∖ran⁡c
16 14 15 ax-mp ⊢recs⁡a∈V⟼C⁡R1⁡dom⁡z∖ran⁡a=recs⁡c∈V⟼C⁡R1⁡dom⁡z∖ran⁡c
17 3 16 eqtri ⊢D=recs⁡c∈V⟼C⁡R1⁡dom⁡z∖ran⁡c
18 fvexd ⊢φ→R1⁡dom⁡z∈V
19 1 2 5 6 7 8 9 10 aomclem2 ⊢φ→∀a∈𝒫R1⁡dom⁡za≠∅→C⁡a∈a
20 neeq1 ⊢a=d→a≠∅↔d≠∅
21 fveq2 ⊢a=d→C⁡a=C⁡d
22 id ⊢a=d→a=d
23 21 22 eleq12d ⊢a=d→C⁡a∈a↔C⁡d∈d
24 20 23 imbi12d ⊢a=d→a≠∅→C⁡a∈a↔d≠∅→C⁡d∈d
25 24 cbvralvw ⊢∀a∈𝒫R1⁡dom⁡za≠∅→C⁡a∈a↔∀d∈𝒫R1⁡dom⁡zd≠∅→C⁡d∈d
26 19 25 sylib ⊢φ→∀d∈𝒫R1⁡dom⁡zd≠∅→C⁡d∈d
27 17 18 26 4 dnwech ⊢φ→EWeR1⁡dom⁡z