Theorem aomclem6 41801

Description: Lemma for dfac11 41804. 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 4005	. 2 ⊢ 𝐴 ⊆ 𝐴
2		aomclem6.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ On)
3	2	adantr 482	. . 3 ⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → 𝐴 ∈ On)
4		sseq1 4008	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝑐 ⊆ 𝐴 ↔ 𝑑 ⊆ 𝐴))
5	4	anbi2d 630	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑑 ⊆ 𝐴)))
6		fveq2 6892	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝐻‘𝑐) = (𝐻‘𝑑))
7		fveq2 6892	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝑅1‘𝑐) = (𝑅1‘𝑑))
8	6, 7	weeq12d 41782	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ (𝐻‘𝑑) We (𝑅1‘𝑑)))
9	5, 8	imbi12d 345	. . . 4 ⊢ (𝑐 = 𝑑 → (((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐)) ↔ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))))
10		sseq1 4008	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝑐 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
11	10	anbi2d 630	. . . . 5 ⊢ (𝑐 = 𝐴 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝐴 ⊆ 𝐴)))
12		fveq2 6892	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝐻‘𝑐) = (𝐻‘𝐴))
13		fveq2 6892	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝑅1‘𝑐) = (𝑅1‘𝐴))
14	12, 13	weeq12d 41782	. . . . 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 5904	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → dom 𝑧 = dom (𝐻 ↾ 𝑐))
23	22	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 = dom (𝐻 ↾ 𝑐))
24		simpl1 1192	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝑐 ∈ On)
25		onss 7772	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ On → 𝑐 ⊆ On)
26		aomclem6.h	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))
27	26	tfr1 8397	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 Fn On
28		fnssres 6674	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻 Fn On ∧ 𝑐 ⊆ On) → (𝐻 ↾ 𝑐) Fn 𝑐)
29	27, 28	mpan 689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ⊆ On → (𝐻 ↾ 𝑐) Fn 𝑐)
30		fndm 6653	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻 ↾ 𝑐) Fn 𝑐 → dom (𝐻 ↾ 𝑐) = 𝑐)
31	24, 25, 29, 30	4syl 19	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom (𝐻 ↾ 𝑐) = 𝑐)
32	23, 31	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 = 𝑐)
33	32, 24	eqeltrd 2834	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ∈ On)
34	32	eleq2d 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑎 ∈ dom 𝑧 ↔ 𝑎 ∈ 𝑐))
35	34	biimpa 478	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ∈ 𝑐)
36		simpll2 1214	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)))
37		simpl3l 1229	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝜑)
38	37	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝜑)
39		onelss 6407	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom 𝑧 ∈ On → (𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧))
40	33, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧))
41	40	imp 408	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ dom 𝑧)
42		simpl3r 1230	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝑐 ⊆ 𝐴)
43	32, 42	eqsstrd 4021	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ⊆ 𝐴)
44	43	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → dom 𝑧 ⊆ 𝐴)
45	41, 44	sstrd 3993	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ 𝐴)
46		sseq1 4008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (𝑑 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴))
47	46	anbi2d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → ((𝜑 ∧ 𝑑 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑎 ⊆ 𝐴)))
48		fveq2 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (𝐻‘𝑑) = (𝐻‘𝑎))
49		fveq2 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (𝑅1‘𝑑) = (𝑅1‘𝑎))
50	48, 49	weeq12d 41782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → ((𝐻‘𝑑) We (𝑅1‘𝑑) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎)))
51	47, 50	imbi12d 345	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑎 → (((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ↔ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝐻‘𝑎) We (𝑅1‘𝑎))))
52	51	rspcva 3611	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝑐 ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) → ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝐻‘𝑎) We (𝑅1‘𝑎)))
53	52	imp 408	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ 𝑐 ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) ∧ (𝜑 ∧ 𝑎 ⊆ 𝐴)) → (𝐻‘𝑎) We (𝑅1‘𝑎))
54	35, 36, 38, 45, 53	syl22anc 838	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝐻‘𝑎) We (𝑅1‘𝑎))
55		fveq1 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎))
56	55	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎))
57		fvres 6911	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ 𝑐 → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎))
58	35, 57	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎))
59	56, 58	eqtrd 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = (𝐻‘𝑎))
60		weeq1 5665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧‘𝑎) = (𝐻‘𝑎) → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎)))
61	59, 60	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎)))
62	54, 61	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) We (𝑅1‘𝑎))
63	62	ralrimiva 3147	. . . . . . . . . . . . . 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 41800	. . . . . . . . . . . . 13 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐺 We (𝑅1‘dom 𝑧))
68	32	fveq2d 6896	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑅1‘dom 𝑧) = (𝑅1‘𝑐))
69		weeq2 5666	. . . . . . . . . . . . . 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 231	. . . . . . . . . . . 12 ⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐺 We (𝑅1‘𝑐))
72	71	ex 414	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → (𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)))
73	72	alrimiv 1931	. . . . . . . . . 10 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ∀𝑧(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)))
74		nfv 1918	. . . . . . . . . . 11 ⊢ Ⅎ𝑑(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐))
75		nfv 1918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧 𝑑 = (𝐻 ↾ 𝑐)
76		nfsbc1v 3798	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧[𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)
77	75, 76	nfim 1900	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))
78		eqeq1 2737	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑑 → (𝑧 = (𝐻 ↾ 𝑐) ↔ 𝑑 = (𝐻 ↾ 𝑐)))
79		sbceq1a 3789	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑑 → (𝐺 We (𝑅1‘𝑐) ↔ [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))
80	78, 79	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑑 → ((𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) ↔ (𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))))
81	74, 77, 80	cbvalv1 2338	. . . . . . . . . 10 ⊢ (∀𝑧(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) ↔ ∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))
82	73, 81	sylib 217	. . . . . . . . 9 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))
83		nfsbc1v 3798	. . . . . . . . . 10 ⊢ Ⅎ𝑑[(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)
84		fnfun 6650	. . . . . . . . . . . 12 ⊢ (𝐻 Fn On → Fun 𝐻)
85	27, 84	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun 𝐻
86		vex 3479	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
87		resfunexg 7217	. . . . . . . . . . 11 ⊢ ((Fun 𝐻 ∧ 𝑐 ∈ V) → (𝐻 ↾ 𝑐) ∈ V)
88	85, 86, 87	mp2an 691	. . . . . . . . . 10 ⊢ (𝐻 ↾ 𝑐) ∈ V
89		sbceq1a 3789	. . . . . . . . . 10 ⊢ (𝑑 = (𝐻 ↾ 𝑐) → ([𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))
90	83, 88, 89	ceqsal 3510	. . . . . . . . 9 ⊢ (∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))
91	82, 90	sylib 217	. . . . . . . 8 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))
92		sbccow 3801	. . . . . . . 8 ⊢ ([(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐))
93	91, 92	sylib 217	. . . . . . 7 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐))
94		nfcsb1v 3919	. . . . . . . . . 10 ⊢ Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺
95		nfcv 2904	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑅1‘𝑐)
96	94, 95	nfwe 5653	. . . . . . . . 9 ⊢ Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)
97		csbeq1a 3908	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → 𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺)
98		weeq1 5665	. . . . . . . . . 10 ⊢ (𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
99	97, 98	syl 17	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
100	96, 99	sbciegf 3817	. . . . . . . 8 ⊢ ((𝐻 ↾ 𝑐) ∈ V → ([(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
101	88, 100	ax-mp 5	. . . . . . 7 ⊢ ([(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))
102	93, 101	sylib 217	. . . . . 6 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))
103		recsval 8404	. . . . . . . . 9 ⊢ (𝑐 ∈ On → (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)))
104	26	fveq1i 6893	. . . . . . . . 9 ⊢ (𝐻‘𝑐) = (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐)
105		fvex 6905	. . . . . . . . . . . . . . 15 ⊢ (𝑅1‘dom 𝑧) ∈ V
106	105, 105	xpex 7740	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)) ∈ V
107	106	inex2 5319	. . . . . . . . . . . . 13 ⊢ (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧))) ∈ V
108	21, 107	eqeltri 2830	. . . . . . . . . . . 12 ⊢ 𝐺 ∈ V
109	108	csbex 5312	. . . . . . . . . . 11 ⊢ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 ∈ V
110		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ V ↦ 𝐺) = (𝑧 ∈ V ↦ 𝐺)
111	110	fvmpts 7002	. . . . . . . . . . 11 ⊢ (((𝐻 ↾ 𝑐) ∈ V ∧ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 ∈ V) → ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺)
112	88, 109, 111	mp2an 691	. . . . . . . . . 10 ⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺
113	26	reseq1i 5978	. . . . . . . . . . 11 ⊢ (𝐻 ↾ 𝑐) = (recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)
114	113	fveq2i 6895	. . . . . . . . . 10 ⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
115	112, 114	eqtr3i 2763	. . . . . . . . 9 ⊢ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))
116	103, 104, 115	3eqtr4g 2798	. . . . . . . 8 ⊢ (𝑐 ∈ On → (𝐻‘𝑐) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺)
117		weeq1 5665	. . . . . . . 8 ⊢ ((𝐻‘𝑐) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
118	116, 117	syl 17	. . . . . . 7 ⊢ (𝑐 ∈ On → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
119	118	3ad2ant1 1134	. . . . . 6 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)))
120	102, 119	mpbird 257	. . . . 5 ⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → (𝐻‘𝑐) We (𝑅1‘𝑐))
121	120	3exp 1120	. . . 4 ⊢ (𝑐 ∈ On → (∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) → ((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐))))
122	9, 15, 121	tfis3 7847	. . 3 ⊢ (𝐴 ∈ On → ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴)))
123	3, 122	mpcom 38	. 2 ⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴))
124	1, 123	mpan2 690	1 ⊢ (𝜑 → (𝐻‘𝐴) We (𝑅1‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088  ∀wal 1540   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  Vcvv 3475  [wsbc 3778  ⦋csb 3894   ∖ cdif 3946   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323  ifcif 4529  𝒫 cpw 4603  {csn 4629  ∪ cuni 4909  ∩ cint 4951   class class class wbr 5149  {copab 5211   ↦ cmpt 5232   E cep 5580   We wwe 5631   × cxp 5675  ^◡ccnv 5676  dom cdm 5677  ran crn 5678   ↾ cres 5679   “ cima 5680  Oncon0 6365  suc csuc 6367  Fun wfun 6538   Fn wfn 6539  ‘cfv 6544  recscrecs 8370  Fincfn 8939  supcsup 9435  𝑅₁cr1 9757  rankcrnk 9758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-map 8822  df-en 8940  df-fin 8943  df-sup 9437  df-r1 9759  df-rank 9760

This theorem is referenced by:  aomclem7  41802