Theorem aomclem6 43504

Description: Lemma for dfac11 43507. Transfinite induction, close over 𝑧. (Contributed by Stefan O'Rear, 20-Jan-2015.)

Hypotheses

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

Assertion

Ref	Expression
aomclem6	⊢ (𝜑 → (𝐻‘𝐴) We (𝑅1‘𝐴))

Distinct variable groups:   𝑦,𝑧,𝑎,𝑏,𝑐,𝑑   𝜑,𝑎,𝑏,𝑐,𝑑,𝑧   𝐶,𝑎,𝑏,𝑐,𝑑   𝐷,𝑎,𝑏,𝑐,𝑑   𝐴,𝑎,𝑏,𝑐,𝑑,𝑧   𝐻,𝑎,𝑏,𝑐,𝑑,𝑧   𝐺,𝑑

Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)   𝐵(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝐶(𝑦,𝑧)   𝐷(𝑦,𝑧)   𝐸(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝐹(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝐺(𝑦,𝑧,𝑎,𝑏,𝑐)   𝐻(𝑦)

Proof of Theorem aomclem6

Step	Hyp	Ref	Expression
1		ssid 3937	. 2 ⊢ 𝐴 ⊆ 𝐴
2		aomclem6.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ On)
3	2	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → 𝐴 ∈ On)
4		sseq1 3940	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝑐 ⊆ 𝐴 ↔ 𝑑 ⊆ 𝐴))
5	4	anbi2d 636	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑑 ⊆ 𝐴)))
6		fveq2 6827	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝐻‘𝑐) = (𝐻‘𝑑))
7		fveq2 6827	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝑅1‘𝑐) = (𝑅1‘𝑑))
8	6, 7	weeq12d 5607	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ (𝐻‘𝑑) We (𝑅1‘𝑑)))
9	5, 8	imbi12d 345	. . . 4 ⊢ (𝑐 = 𝑑 → (((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐)) ↔ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))))
10		sseq1 3940	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝑐 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
11	10	anbi2d 636	. . . . 5 ⊢ (𝑐 = 𝐴 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝐴 ⊆ 𝐴)))
12		fveq2 6827	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝐻‘𝑐) = (𝐻‘𝐴))
13		fveq2 6827	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝑅1‘𝑐) = (𝑅1‘𝐴))
14	12, 13	weeq12d 5607	. . . . 5 ⊢ (𝑐 = 𝐴 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ (𝐻‘𝐴) We (𝑅1‘𝐴)))
15	11, 14	imbi12d 345	. . . 4 ⊢ (𝑐 = 𝐴 → (((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐)) ↔ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴))))
16		aomclem6.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}
17		aomclem6.c	. . . . . . . . . . . . . 14 ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))
18		aomclem6.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))
19		aomclem6.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = {⟨𝑎, 𝑏⟩ ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})}
20		aomclem6.f	. . . . . . . . . . . . . 14 ⊢ 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}
21		aomclem6.g	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))
22		dmeq 5845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → dom 𝑧 = dom (𝐻 ↾ 𝑐))
23	22	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 = dom (𝐻 ↾ 𝑐))
24		simpl1 1198	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝑐 ∈ On)
25		onss 7728	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ On → 𝑐 ⊆ On)
26		aomclem6.h	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))
27	26	tfr1 8326	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 Fn On
28		fnssres 6608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻 Fn On ∧ 𝑐 ⊆ On) → (𝐻 ↾ 𝑐) Fn 𝑐)
29	27, 28	mpan 696	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ⊆ On → (𝐻 ↾ 𝑐) Fn 𝑐)
30		fndm 6588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻 ↾ 𝑐) Fn 𝑐 → dom (𝐻 ↾ 𝑐) = 𝑐)
31	24, 25, 29, 30	4syl 19	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom (𝐻 ↾ 𝑐) = 𝑐)
32	23, 31	eqtrd 2774	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 = 𝑐)
33	32, 24	eqeltrd 2839	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ∈ On)
34	32	eleq2d 2825	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑎 ∈ dom 𝑧 ↔ 𝑎 ∈ 𝑐))
35	34	biimpa 477	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ∈ 𝑐)
36		simpll2 1220	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)))
37		simpl3l 1235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝜑)
38	37	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝜑)
39		onelss 6352	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom 𝑧 ∈ On → (𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧))
40	33, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧))
41	40	imp 407	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ dom 𝑧)
42		simpl3r 1236	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝑐 ⊆ 𝐴)
43	32, 42	eqsstrd 3949	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ⊆ 𝐴)
44	43	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → dom 𝑧 ⊆ 𝐴)
45	41, 44	sstrd 3925	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ 𝐴)
46		sseq1 3940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (𝑑 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴))
47	46	anbi2d 636	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → ((𝜑 ∧ 𝑑 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑎 ⊆ 𝐴)))
48		fveq2 6827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (𝐻‘𝑑) = (𝐻‘𝑎))
49		fveq2 6827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (𝑅1‘𝑑) = (𝑅1‘𝑎))
50	48, 49	weeq12d 5607	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → ((𝐻‘𝑑) We (𝑅1‘𝑑) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎)))
51	47, 50	imbi12d 345	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑎 → (((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ↔ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝐻‘𝑎) We (𝑅1‘𝑎))))
52	51	rspcva 3558	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝑐 ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) → ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝐻‘𝑎) We (𝑅1‘𝑎)))
53	52	imp 407	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ 𝑐 ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) ∧ (𝜑 ∧ 𝑎 ⊆ 𝐴)) → (𝐻‘𝑎) We (𝑅1‘𝑎))
54	35, 36, 38, 45, 53	syl22anc 844	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝐻‘𝑎) We (𝑅1‘𝑎))
55		fveq1 6826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎))
56	55	ad2antlr 733	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎))
57		fvres 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ 𝑐 → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎))
58	35, 57	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎))
59	56, 58	eqtrd 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = (𝐻‘𝑎))
60		weeq1 5605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧‘𝑎) = (𝐻‘𝑎) → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎)))
61	59, 60	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎)))
62	54, 61	mpbird 258	. . . . . . . . . . . . . . 15 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) We (𝑅1‘𝑎))
63	62	ralrimiva 3131	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))
64	37, 2	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐴 ∈ On)
65		aomclem6.y	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))
66	37, 65	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))
67	16, 17, 18, 19, 20, 21, 33, 63, 64, 43, 66	aomclem5 43503	. . . . . . . . . . . . 13 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐺 We (𝑅1‘dom 𝑧))
68	32	fveq2d 6831	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑅1‘dom 𝑧) = (𝑅1‘𝑐))
69		weeq2 5606	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘dom 𝑧) = (𝑅1‘𝑐) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1‘𝑐)))
70	68, 69	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1‘𝑐)))
71	67, 70	mpbid 233	. . . . . . . . . . . 12 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐺 We (𝑅1‘𝑐))
72	71	ex 413	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → (𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)))
73	72	alrimiv 1934	. . . . . . . . . 10 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ∀𝑧(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)))
74		nfv 1921	. . . . . . . . . . 11 ⊢ Ⅎ𝑑(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐))
75		nfv 1921	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧 𝑑 = (𝐻 ↾ 𝑐)
76		nfsbc1v 3743	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧[𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)
77	75, 76	nfim 1903	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))
78		eqeq1 2743	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑑 → (𝑧 = (𝐻 ↾ 𝑐) ↔ 𝑑 = (𝐻 ↾ 𝑐)))
79		sbceq1a 3734	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑑 → (𝐺 We (𝑅1‘𝑐) ↔ [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))
80	78, 79	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑑 → ((𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) ↔ (𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))))
81	74, 77, 80	cbvalv1 2349	. . . . . . . . . 10 ⊢ (∀𝑧(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) ↔ ∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))
82	73, 81	sylib 219	. . . . . . . . 9 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))
83		nfsbc1v 3743	. . . . . . . . . 10 ⊢ Ⅎ𝑑[(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)
84		fnfun 6585	. . . . . . . . . . . 12 ⊢ (𝐻 Fn On → Fun 𝐻)
85	27, 84	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun 𝐻
86		vex 3435	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
87		resfunexg 7159	. . . . . . . . . . 11 ⊢ ((Fun 𝐻 ∧ 𝑐 ∈ V) → (𝐻 ↾ 𝑐) ∈ V)
88	85, 86, 87	mp2an 698	. . . . . . . . . 10 ⊢ (𝐻 ↾ 𝑐) ∈ V
89		sbceq1a 3734	. . . . . . . . . 10 ⊢ (𝑑 = (𝐻 ↾ 𝑐) → ([𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))
90	83, 88, 89	ceqsal 3468	. . . . . . . . 9 ⊢ (∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))
91	82, 90	sylib 219	. . . . . . . 8 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))
92		sbccow 3746	. . . . . . . 8 ⊢ ([(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐))
93	91, 92	sylib 219	. . . . . . 7 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐))
94		nfcsb1v 3855	. . . . . . . . . 10 ⊢ Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺
95		nfcv 2901	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑅1‘𝑐)
96	94, 95	nfwe 5593	. . . . . . . . 9 ⊢ Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)
97		csbeq1a 3845	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → 𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺)
98		weeq1 5605	. . . . . . . . . 10 ⊢ (𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
99	97, 98	syl 17	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
100	96, 99	sbciegf 3761	. . . . . . . 8 ⊢ ((𝐻 ↾ 𝑐) ∈ V → ([(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
101	88, 100	ax-mp 5	. . . . . . 7 ⊢ ([(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))
102	93, 101	sylib 219	. . . . . 6 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))
103		recsval 8333	. . . . . . . . 9 ⊢ (𝑐 ∈ On → (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)))
104	26	fveq1i 6828	. . . . . . . . 9 ⊢ (𝐻‘𝑐) = (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐)
105		fvex 6840	. . . . . . . . . . . . . . 15 ⊢ (𝑅1‘dom 𝑧) ∈ V
106	105, 105	xpex 7696	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)) ∈ V
107	106	inex2 5246	. . . . . . . . . . . . 13 ⊢ (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧))) ∈ V
108	21, 107	eqeltri 2835	. . . . . . . . . . . 12 ⊢ 𝐺 ∈ V
109	108	csbex 5233	. . . . . . . . . . 11 ⊢ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 ∈ V
110		eqid 2739	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ V ↦ 𝐺) = (𝑧 ∈ V ↦ 𝐺)
111	110	fvmpts 6939	. . . . . . . . . . 11 ⊢ (((𝐻 ↾ 𝑐) ∈ V ∧ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 ∈ V) → ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺)
112	88, 109, 111	mp2an 698	. . . . . . . . . 10 ⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺
113	26	reseq1i 5927	. . . . . . . . . . 11 ⊢ (𝐻 ↾ 𝑐) = (recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)
114	113	fveq2i 6830	. . . . . . . . . 10 ⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
115	112, 114	eqtr3i 2764	. . . . . . . . 9 ⊢ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
116	103, 104, 115	3eqtr4g 2799	. . . . . . . 8 ⊢ (𝑐 ∈ On → (𝐻‘𝑐) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺)
117		weeq1 5605	. . . . . . . 8 ⊢ ((𝐻‘𝑐) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
118	116, 117	syl 17	. . . . . . 7 ⊢ (𝑐 ∈ On → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
119	118	3ad2ant1 1139	. . . . . 6 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
120	102, 119	mpbird 258	. . . . 5 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → (𝐻‘𝑐) We (𝑅1‘𝑐))
121	120	3exp 1125	. . . 4 ⊢ (𝑐 ∈ On → (∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) → ((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐))))
122	9, 15, 121	tfis3 7798	. . 3 ⊢ (𝐴 ∈ On → ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴)))
123	3, 122	mpcom 38	. 2 ⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴))
124	1, 123	mpan2 697	1 ⊢ (𝜑 → (𝐻‘𝐴) We (𝑅1‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092  ∀wal 1545   = wceq 1547   ∈ wcel 2119   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  Vcvv 3431  [wsbc 3723  ⦋csb 3831   ∖ cdif 3880   ∩ cin 3882   ⊆ wss 3883  ∅c0 4261  ifcif 4454  𝒫 cpw 4529  {csn 4555  ∪ cuni 4838  ∩ cint 4877   class class class wbr 5072  {copab 5134   ↦ cmpt 5153   E cep 5517   We wwe 5570   × cxp 5616  ^◡ccnv 5617  dom cdm 5618  ran crn 5619   ↾ cres 5620   “ cima 5621  Oncon0 6310  suc csuc 6312  Fun wfun 6479   Fn wfn 6480  ‘cfv 6485  recscrecs 8300  Fincfn 8883  supcsup 9343  𝑅₁cr1 9677  rankcrnk 9678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-map 8765  df-en 8884  df-fin 8887  df-sup 9345  df-r1 9679  df-rank 9680

This theorem is referenced by:  aomclem7  43505