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	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
	aomclem3.c	⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
	aomclem3.d	⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) )
	aomclem3.e	⊢ 𝐸 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) }
	aomclem3.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
	aomclem3.su	⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
	aomclem3.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
	aomclem3.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	aomclem3.za	⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
	aomclem3.y	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
Assertion	aomclem3	⊢ ( 𝜑 → 𝐸 We ( 𝑅1 ‘ dom 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		aomclem3.b	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
2		aomclem3.c	⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
3		aomclem3.d	⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) )
4		aomclem3.e	⊢ 𝐸 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) }
5		aomclem3.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
6		aomclem3.su	⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
7		aomclem3.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
8		aomclem3.a	⊢ ( 𝜑 → 𝐴 ∈ On )
9		aomclem3.za	⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
10		aomclem3.y	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
11		rneq	⊢ ( 𝑎 = 𝑐 → ran 𝑎 = ran 𝑐 )
12	11	difeq2d	⊢ ( 𝑎 = 𝑐 → ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) = ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) )
13	12	fveq2d	⊢ ( 𝑎 = 𝑐 → ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) = ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) )
14	13	cbvmptv	⊢ ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) = ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) )
15		recseq	⊢ ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) = ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) ) → recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) ) = recs ( ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) ) ) )
16	14 15	ax-mp	⊢ recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) ) = recs ( ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) ) )
17	3 16	eqtri	⊢ 𝐷 = recs ( ( 𝑐 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑐 ) ) ) )
18		fvexd	⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) ∈ V )
19	1 2 5 6 7 8 9 10	aomclem2	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) )
20		neeq1	⊢ ( 𝑎 = 𝑑 → ( 𝑎 ≠ ∅ ↔ 𝑑 ≠ ∅ ) )
21		fveq2	⊢ ( 𝑎 = 𝑑 → ( 𝐶 ‘ 𝑎 ) = ( 𝐶 ‘ 𝑑 ) )
22		id	⊢ ( 𝑎 = 𝑑 → 𝑎 = 𝑑 )
23	21 22	eleq12d	⊢ ( 𝑎 = 𝑑 → ( ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ↔ ( 𝐶 ‘ 𝑑 ) ∈ 𝑑 ) )
24	20 23	imbi12d	⊢ ( 𝑎 = 𝑑 → ( ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) ↔ ( 𝑑 ≠ ∅ → ( 𝐶 ‘ 𝑑 ) ∈ 𝑑 ) ) )
25	24	cbvralvw	⊢ ( ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) ↔ ∀ 𝑑 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑑 ≠ ∅ → ( 𝐶 ‘ 𝑑 ) ∈ 𝑑 ) )
26	19 25	sylib	⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑑 ≠ ∅ → ( 𝐶 ‘ 𝑑 ) ∈ 𝑑 ) )
27	17 18 26 4	dnwech	⊢ ( 𝜑 → 𝐸 We ( 𝑅1 ‘ dom 𝑧 ) )