Theorem aomclem6 43511

Description: Lemma for dfac11 43514. 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 3944	. 2 ⊢ 𝐴 ⊆ 𝐴
2		aomclem6.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ On)
3	2	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → 𝐴 ∈ On)
4		sseq1 3947	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝑐 ⊆ 𝐴 ↔ 𝑑 ⊆ 𝐴))
5	4	anbi2d 636	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑑 ⊆ 𝐴)))
6		fveq2 6834	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝐻‘𝑐) = (𝐻‘𝑑))
7		fveq2 6834	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝑅1‘𝑐) = (𝑅1‘𝑑))
8	6, 7	weeq12d 5614	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ (𝐻‘𝑑) We (𝑅1‘𝑑)))
9	5, 8	imbi12d 345	. . . 4 ⊢ (𝑐 = 𝑑 → (((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐)) ↔ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))))
10		sseq1 3947	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝑐 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
11	10	anbi2d 636	. . . . 5 ⊢ (𝑐 = 𝐴 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝐴 ⊆ 𝐴)))
12		fveq2 6834	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝐻‘𝑐) = (𝐻‘𝐴))
13		fveq2 6834	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝑅1‘𝑐) = (𝑅1‘𝐴))
14	12, 13	weeq12d 5614	. . . . 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 5852	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → dom 𝑧 = dom (𝐻 ↾ 𝑐))
23	22	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 = dom (𝐻 ↾ 𝑐))
24		simpl1 1198	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝑐 ∈ On)
25		onss 7735	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ On → 𝑐 ⊆ On)
26		aomclem6.h	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))
27	26	tfr1 8333	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 Fn On
28		fnssres 6615	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻 Fn On ∧ 𝑐 ⊆ On) → (𝐻 ↾ 𝑐) Fn 𝑐)
29	27, 28	mpan 696	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ⊆ On → (𝐻 ↾ 𝑐) Fn 𝑐)
30		fndm 6595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻 ↾ 𝑐) Fn 𝑐 → dom (𝐻 ↾ 𝑐) = 𝑐)
31	24, 25, 29, 30	4syl 19	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom (𝐻 ↾ 𝑐) = 𝑐)
32	23, 31	eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 = 𝑐)
33	32, 24	eqeltrd 2840	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ∈ On)
34	32	eleq2d 2826	. . . . . . . . . . . . . . . . . 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 6359	. . . . . . . . . . . . . . . . . . . 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 3956	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ⊆ 𝐴)
44	43	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → dom 𝑧 ⊆ 𝐴)
45	41, 44	sstrd 3932	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ 𝐴)
46		sseq1 3947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (𝑑 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴))
47	46	anbi2d 636	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → ((𝜑 ∧ 𝑑 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑎 ⊆ 𝐴)))
48		fveq2 6834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (𝐻‘𝑑) = (𝐻‘𝑎))
49		fveq2 6834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (𝑅1‘𝑑) = (𝑅1‘𝑎))
50	48, 49	weeq12d 5614	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → ((𝐻‘𝑑) We (𝑅1‘𝑑) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎)))
51	47, 50	imbi12d 345	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑎 → (((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ↔ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝐻‘𝑎) We (𝑅1‘𝑎))))
52	51	rspcva 3565	. . . . . . . . . . . . . . . . . 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 6833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎))
56	55	ad2antlr 733	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎))
57		fvres 6853	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ 𝑐 → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎))
58	35, 57	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎))
59	56, 58	eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = (𝐻‘𝑎))
60		weeq1 5612	. . . . . . . . . . . . . . . . 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 3132	. . . . . . . . . . . . . 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 43510	. . . . . . . . . . . . 13 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐺 We (𝑅1‘dom 𝑧))
68	32	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑅1‘dom 𝑧) = (𝑅1‘𝑐))
69		weeq2 5613	. . . . . . . . . . . . . 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 3750	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧[𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)
77	75, 76	nfim 1903	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))
78		eqeq1 2744	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑑 → (𝑧 = (𝐻 ↾ 𝑐) ↔ 𝑑 = (𝐻 ↾ 𝑐)))
79		sbceq1a 3741	. . . . . . . . . . . 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 3750	. . . . . . . . . 10 ⊢ Ⅎ𝑑[(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)
84		fnfun 6592	. . . . . . . . . . . 12 ⊢ (𝐻 Fn On → Fun 𝐻)
85	27, 84	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun 𝐻
86		vex 3436	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
87		resfunexg 7166	. . . . . . . . . . 11 ⊢ ((Fun 𝐻 ∧ 𝑐 ∈ V) → (𝐻 ↾ 𝑐) ∈ V)
88	85, 86, 87	mp2an 698	. . . . . . . . . 10 ⊢ (𝐻 ↾ 𝑐) ∈ V
89		sbceq1a 3741	. . . . . . . . . 10 ⊢ (𝑑 = (𝐻 ↾ 𝑐) → ([𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))
90	83, 88, 89	ceqsal 3470	. . . . . . . . 9 ⊢ (∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))
91	82, 90	sylib 219	. . . . . . . 8 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))
92		sbccow 3753	. . . . . . . 8 ⊢ ([(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐))
93	91, 92	sylib 219	. . . . . . 7 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐))
94		nfcsb1v 3862	. . . . . . . . . 10 ⊢ Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺
95		nfcv 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑅1‘𝑐)
96	94, 95	nfwe 5600	. . . . . . . . 9 ⊢ Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)
97		csbeq1a 3852	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → 𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺)
98		weeq1 5612	. . . . . . . . . 10 ⊢ (𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
99	97, 98	syl 17	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
100	96, 99	sbciegf 3768	. . . . . . . 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 8340	. . . . . . . . 9 ⊢ (𝑐 ∈ On → (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)))
104	26	fveq1i 6835	. . . . . . . . 9 ⊢ (𝐻‘𝑐) = (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐)
105		fvex 6847	. . . . . . . . . . . . . . 15 ⊢ (𝑅1‘dom 𝑧) ∈ V
106	105, 105	xpex 7703	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)) ∈ V
107	106	inex2 5253	. . . . . . . . . . . . 13 ⊢ (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧))) ∈ V
108	21, 107	eqeltri 2836	. . . . . . . . . . . 12 ⊢ 𝐺 ∈ V
109	108	csbex 5240	. . . . . . . . . . 11 ⊢ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 ∈ V
110		eqid 2740	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ V ↦ 𝐺) = (𝑧 ∈ V ↦ 𝐺)
111	110	fvmpts 6946	. . . . . . . . . . 11 ⊢ (((𝐻 ↾ 𝑐) ∈ V ∧ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 ∈ V) → ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺)
112	88, 109, 111	mp2an 698	. . . . . . . . . 10 ⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺
113	26	reseq1i 5934	. . . . . . . . . . 11 ⊢ (𝐻 ↾ 𝑐) = (recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)
114	113	fveq2i 6837	. . . . . . . . . 10 ⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
115	112, 114	eqtr3i 2765	. . . . . . . . 9 ⊢ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
116	103, 104, 115	3eqtr4g 2800	. . . . . . . 8 ⊢ (𝑐 ∈ On → (𝐻‘𝑐) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺)
117		weeq1 5612	. . . . . . . 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 7805	. . 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 2935  ∀wral 3054  ∃wrex 3064  Vcvv 3432  [wsbc 3730  ⦋csb 3838   ∖ cdif 3887   ∩ cin 3889   ⊆ wss 3890  ∅c0 4268  ifcif 4461  𝒫 cpw 4536  {csn 4562  ∪ cuni 4845  ∩ cint 4884   class class class wbr 5079  {copab 5141   ↦ cmpt 5160   E cep 5524   We wwe 5577   × cxp 5623  ^◡ccnv 5624  dom cdm 5625  ran crn 5626   ↾ cres 5627   “ cima 5628  Oncon0 6317  suc csuc 6319  Fun wfun 6486   Fn wfn 6487  ‘cfv 6492  recscrecs 8307  Fincfn 8890  supcsup 9350  𝑅₁cr1 9684  rankcrnk 9685

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 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

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 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-1st 7938  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-2o 8403  df-map 8772  df-en 8891  df-fin 8894  df-sup 9352  df-r1 9686  df-rank 9687

This theorem is referenced by:  aomclem7  43512