Theorem aomclem5

Description: Lemma for dfac11 . Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Hypotheses	aomclem5.b	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
	aomclem5.c	⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
	aomclem5.d	⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) )
	aomclem5.e	⊢ 𝐸 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) }
	aomclem5.f	⊢ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) }
	aomclem5.g	⊢ 𝐺 = ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) )
	aomclem5.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
	aomclem5.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
	aomclem5.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	aomclem5.za	⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
	aomclem5.y	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
Assertion	aomclem5	⊢ ( 𝜑 → 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		aomclem5.b	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
2		aomclem5.c	⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
3		aomclem5.d	⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) )
4		aomclem5.e	⊢ 𝐸 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) }
5		aomclem5.f	⊢ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) }
6		aomclem5.g	⊢ 𝐺 = ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) )
7		aomclem5.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
8		aomclem5.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
9		aomclem5.a	⊢ ( 𝜑 → 𝐴 ∈ On )
10		aomclem5.za	⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
11		aomclem5.y	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
12	7	adantr	⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 ∈ On )
13		simpr	⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 = ∪ dom 𝑧 )
14	8	adantr	⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
15	5 12 13 14	aomclem4	⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → 𝐹 We ( 𝑅1 ‘ dom 𝑧 ) )
16		iftrue	⊢ ( dom 𝑧 = ∪ dom 𝑧 → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) = 𝐹 )
17	16	adantl	⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) = 𝐹 )
18		eqidd	⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → ( 𝑅1 ‘ dom 𝑧 ) = ( 𝑅1 ‘ dom 𝑧 ) )
19	17 18	weeq12d	⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐹 We ( 𝑅1 ‘ dom 𝑧 ) ) )
20	15 19	mpbird	⊢ ( ( 𝜑 ∧ dom 𝑧 = ∪ dom 𝑧 ) → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) )
21	7	adantr	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 ∈ On )
22		eloni	⊢ ( dom 𝑧 ∈ On → Ord dom 𝑧 )
23		orduniorsuc	⊢ ( Ord dom 𝑧 → ( dom 𝑧 = ∪ dom 𝑧 ∨ dom 𝑧 = suc ∪ dom 𝑧 ) )
24	7 22 23	3syl	⊢ ( 𝜑 → ( dom 𝑧 = ∪ dom 𝑧 ∨ dom 𝑧 = suc ∪ dom 𝑧 ) )
25	24	orcanai	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 = suc ∪ dom 𝑧 )
26	8	adantr	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
27	9	adantr	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → 𝐴 ∈ On )
28	10	adantr	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → dom 𝑧 ⊆ 𝐴 )
29	11	adantr	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
30	1 2 3 4 21 25 26 27 28 29	aomclem3	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → 𝐸 We ( 𝑅1 ‘ dom 𝑧 ) )
31		iffalse	⊢ ( ¬ dom 𝑧 = ∪ dom 𝑧 → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) = 𝐸 )
32	31	adantl	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) = 𝐸 )
33		eqidd	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → ( 𝑅1 ‘ dom 𝑧 ) = ( 𝑅1 ‘ dom 𝑧 ) )
34	32 33	weeq12d	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐸 We ( 𝑅1 ‘ dom 𝑧 ) ) )
35	30 34	mpbird	⊢ ( ( 𝜑 ∧ ¬ dom 𝑧 = ∪ dom 𝑧 ) → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) )
36	20 35	pm2.61dan	⊢ ( 𝜑 → if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) )
37		weinxp	⊢ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) We ( 𝑅1 ‘ dom 𝑧 ) ↔ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) We ( 𝑅1 ‘ dom 𝑧 ) )
38	36 37	sylib	⊢ ( 𝜑 → ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) We ( 𝑅1 ‘ dom 𝑧 ) )
39		weeq1	⊢ ( 𝐺 = ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) → ( 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) ↔ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) We ( 𝑅1 ‘ dom 𝑧 ) ) )
40	6 39	ax-mp	⊢ ( 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) ↔ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) We ( 𝑅1 ‘ dom 𝑧 ) )
41	38 40	sylibr	⊢ ( 𝜑 → 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) )