aomclem6

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

	Ref	Expression
Hypotheses	aomclem6.b	$⊢ B = \{⟨a, b⟩ \| \exists c \in R_{1} (⋃ dom z) ((c \in b \land \neg c \in a) \land \forall d \in R_{1} (⋃ dom z) (d z (⋃ dom z) c \to (d \in a \leftrightarrow d \in b)))\}$
	aomclem6.c	$⊢ C = (a \in V ⟼ sup (y (a), R_{1} (dom z), B))$
	aomclem6.d	$⊢ D = recs ((a \in V ⟼ C (R_{1} (dom z) ∖ ran a)))$
	aomclem6.e	$⊢ E = \{⟨a, b⟩ \| ⋂ D^{-1} [\{a\}] \in ⋂ D^{-1} [\{b\}]\}$
	aomclem6.f	$⊢ F = \{⟨a, b⟩ \| (rank (a) E rank (b) \lor (rank (a) = rank (b) \land a z (suc rank (a)) b))\}$
	aomclem6.g	$⊢ G = if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z))$
	aomclem6.h	$⊢ H = recs ((z \in V ⟼ G))$
	aomclem6.a	$⊢ φ \to A \in On$
	aomclem6.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
Assertion	aomclem6	$⊢ φ \to H (A) We R_{1} (A)$

Proof

Step	Hyp	Ref	Expression
1		aomclem6.b	$⊢ B = \{⟨a, b⟩ \| \exists c \in R_{1} (⋃ dom z) ((c \in b \land \neg c \in a) \land \forall d \in R_{1} (⋃ dom z) (d z (⋃ dom z) c \to (d \in a \leftrightarrow d \in b)))\}$
2		aomclem6.c	$⊢ C = (a \in V ⟼ sup (y (a), R_{1} (dom z), B))$
3		aomclem6.d	$⊢ D = recs ((a \in V ⟼ C (R_{1} (dom z) ∖ ran a)))$
4		aomclem6.e	$⊢ E = \{⟨a, b⟩ \| ⋂ D^{-1} [\{a\}] \in ⋂ D^{-1} [\{b\}]\}$
5		aomclem6.f	$⊢ F = \{⟨a, b⟩ \| (rank (a) E rank (b) \lor (rank (a) = rank (b) \land a z (suc rank (a)) b))\}$
6		aomclem6.g	$⊢ G = if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z))$
7		aomclem6.h	$⊢ H = recs ((z \in V ⟼ G))$
8		aomclem6.a	$⊢ φ \to A \in On$
9		aomclem6.y	$⊢ φ \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
10		ssid	$⊢ A \subseteq A$
11	8	adantr	$⊢ (φ \land A \subseteq A) \to A \in On$
12		sseq1	$⊢ c = d \to (c \subseteq A \leftrightarrow d \subseteq A)$
13	12	anbi2d	$⊢ c = d \to ((φ \land c \subseteq A) \leftrightarrow (φ \land d \subseteq A))$
14		fveq2	$⊢ c = d \to H (c) = H (d)$
15		fveq2	$⊢ c = d \to R_{1} (c) = R_{1} (d)$
16	14 15	weeq12d	$⊢ c = d \to (H (c) We R_{1} (c) \leftrightarrow H (d) We R_{1} (d))$
17	13 16	imbi12d	$⊢ c = d \to (((φ \land c \subseteq A) \to H (c) We R_{1} (c)) \leftrightarrow ((φ \land d \subseteq A) \to H (d) We R_{1} (d)))$
18		sseq1	$⊢ c = A \to (c \subseteq A \leftrightarrow A \subseteq A)$
19	18	anbi2d	$⊢ c = A \to ((φ \land c \subseteq A) \leftrightarrow (φ \land A \subseteq A))$
20		fveq2	$⊢ c = A \to H (c) = H (A)$
21		fveq2	$⊢ c = A \to R_{1} (c) = R_{1} (A)$
22	20 21	weeq12d	$⊢ c = A \to (H (c) We R_{1} (c) \leftrightarrow H (A) We R_{1} (A))$
23	19 22	imbi12d	$⊢ c = A \to (((φ \land c \subseteq A) \to H (c) We R_{1} (c)) \leftrightarrow ((φ \land A \subseteq A) \to H (A) We R_{1} (A)))$
24		dmeq	$⊢ z = {H ↾}_{c} \to dom z = dom ({H ↾}_{c})$
25	24	adantl	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to dom z = dom ({H ↾}_{c})$
26		simpl1	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to c \in On$
27		onss	$⊢ c \in On \to c \subseteq On$
28	7	tfr1	$⊢ H Fn On$
29		fnssres	$⊢ (H Fn On \land c \subseteq On) \to ({H ↾}_{c}) Fn c$
30	28 29	mpan	$⊢ c \subseteq On \to ({H ↾}_{c}) Fn c$
31		fndm	$⊢ ({H ↾}_{c}) Fn c \to dom ({H ↾}_{c}) = c$
32	26 27 30 31	4syl	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to dom ({H ↾}_{c}) = c$
33	25 32	eqtrd	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to dom z = c$
34	33 26	eqeltrd	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to dom z \in On$
35	33	eleq2d	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to (a \in dom z \leftrightarrow a \in c)$
36	35	biimpa	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to a \in c$
37		simpll2	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d))$
38		simpl3l	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to φ$
39	38	adantr	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to φ$
40		onelss	$⊢ dom z \in On \to (a \in dom z \to a \subseteq dom z)$
41	34 40	syl	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to (a \in dom z \to a \subseteq dom z)$
42	41	imp	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to a \subseteq dom z$
43		simpl3r	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to c \subseteq A$
44	33 43	eqsstrd	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to dom z \subseteq A$
45	44	adantr	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to dom z \subseteq A$
46	42 45	sstrd	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to a \subseteq A$
47		sseq1	$⊢ d = a \to (d \subseteq A \leftrightarrow a \subseteq A)$
48	47	anbi2d	$⊢ d = a \to ((φ \land d \subseteq A) \leftrightarrow (φ \land a \subseteq A))$
49		fveq2	$⊢ d = a \to H (d) = H (a)$
50		fveq2	$⊢ d = a \to R_{1} (d) = R_{1} (a)$
51	49 50	weeq12d	$⊢ d = a \to (H (d) We R_{1} (d) \leftrightarrow H (a) We R_{1} (a))$
52	48 51	imbi12d	$⊢ d = a \to (((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \leftrightarrow ((φ \land a \subseteq A) \to H (a) We R_{1} (a)))$
53	52	rspcva	$⊢ (a \in c \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d))) \to ((φ \land a \subseteq A) \to H (a) We R_{1} (a))$
54	53	imp	$⊢ ((a \in c \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d))) \land (φ \land a \subseteq A)) \to H (a) We R_{1} (a)$
55	36 37 39 46 54	syl22anc	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to H (a) We R_{1} (a)$
56		fveq1	$⊢ z = {H ↾}_{c} \to z (a) = ({H ↾}_{c}) (a)$
57	56	ad2antlr	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to z (a) = ({H ↾}_{c}) (a)$
58		fvres	$⊢ a \in c \to ({H ↾}_{c}) (a) = H (a)$
59	36 58	syl	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to ({H ↾}_{c}) (a) = H (a)$
60	57 59	eqtrd	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to z (a) = H (a)$
61		weeq1	$⊢ z (a) = H (a) \to (z (a) We R_{1} (a) \leftrightarrow H (a) We R_{1} (a))$
62	60 61	syl	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to (z (a) We R_{1} (a) \leftrightarrow H (a) We R_{1} (a))$
63	55 62	mpbird	$⊢ (((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \land a \in dom z) \to z (a) We R_{1} (a)$
64	63	ralrimiva	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to \forall a \in dom z z (a) We R_{1} (a)$
65	38 8	syl	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to A \in On$
66	38 9	syl	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to \forall a \in 𝒫 R_{1} (A) (a \neq \emptyset \to y (a) \in ((𝒫 a \cap Fin) ∖ \{\emptyset\}))$
67	1 2 3 4 5 6 34 64 65 44 66	aomclem5	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to G We R_{1} (dom z)$
68	33	fveq2d	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to R_{1} (dom z) = R_{1} (c)$
69		weeq2	$⊢ R_{1} (dom z) = R_{1} (c) \to (G We R_{1} (dom z) \leftrightarrow G We R_{1} (c))$
70	68 69	syl	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to (G We R_{1} (dom z) \leftrightarrow G We R_{1} (c))$
71	67 70	mpbid	$⊢ ((c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \land z = {H ↾}_{c}) \to G We R_{1} (c)$
72	71	ex	$⊢ (c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \to (z = {H ↾}_{c} \to G We R_{1} (c))$
73	72	alrimiv	$⊢ (c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \to \forall z (z = {H ↾}_{c} \to G We R_{1} (c))$
74		nfv	$⊢ Ⅎ d (z = {H ↾}_{c} \to G We R_{1} (c))$
75		nfv	$⊢ Ⅎ z d = {H ↾}_{c}$
76		nfsbc1v	$⊢ Ⅎ z \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c)$
77	75 76	nfim	$⊢ Ⅎ z (d = {H ↾}_{c} \to \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c))$
78		eqeq1	$⊢ z = d \to (z = {H ↾}_{c} \leftrightarrow d = {H ↾}_{c})$
79		sbceq1a	$⊢ z = d \to (G We R_{1} (c) \leftrightarrow \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c))$
80	78 79	imbi12d	$⊢ z = d \to ((z = {H ↾}_{c} \to G We R_{1} (c)) \leftrightarrow (d = {H ↾}_{c} \to \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c)))$
81	74 77 80	cbvalv1	$⊢ \forall z (z = {H ↾}_{c} \to G We R_{1} (c)) \leftrightarrow \forall d (d = {H ↾}_{c} \to \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c))$
82	73 81	sylib	$⊢ (c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \to \forall d (d = {H ↾}_{c} \to \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c))$
83		nfsbc1v	$⊢ Ⅎ d \underset{˙}{[} ({H ↾}_{c}) / d \underset{˙}{]} \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c)$
84		fnfun	$⊢ H Fn On \to Fun H$
85	28 84	ax-mp	$⊢ Fun H$
86		vex	$⊢ c \in V$
87		resfunexg	$⊢ (Fun H \land c \in V) \to {H ↾}_{c} \in V$
88	85 86 87	mp2an	$⊢ {H ↾}_{c} \in V$
89		sbceq1a	$⊢ d = {H ↾}_{c} \to (\underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c) \leftrightarrow \underset{˙}{[} ({H ↾}_{c}) / d \underset{˙}{]} \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c))$
90	83 88 89	ceqsal	$⊢ \forall d (d = {H ↾}_{c} \to \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c)) \leftrightarrow \underset{˙}{[} ({H ↾}_{c}) / d \underset{˙}{]} \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c)$
91	82 90	sylib	$⊢ (c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \to \underset{˙}{[} ({H ↾}_{c}) / d \underset{˙}{]} \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c)$
92		sbccow	$⊢ \underset{˙}{[} ({H ↾}_{c}) / d \underset{˙}{]} \underset{˙}{[} d / z \underset{˙}{]} G We R_{1} (c) \leftrightarrow \underset{˙}{[} ({H ↾}_{c}) / z \underset{˙}{]} G We R_{1} (c)$
93	91 92	sylib	$⊢ (c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \to \underset{˙}{[} ({H ↾}_{c}) / z \underset{˙}{]} G We R_{1} (c)$
94		nfcsb1v	$⊢ \underline{Ⅎ} z ⦋ ({H ↾}_{c}) / z ⦌ G$
95		nfcv	$⊢ \underline{Ⅎ} z R_{1} (c)$
96	94 95	nfwe	$⊢ Ⅎ z ⦋ ({H ↾}_{c}) / z ⦌ G We R_{1} (c)$
97		csbeq1a	$⊢ z = {H ↾}_{c} \to G = ⦋ ({H ↾}_{c}) / z ⦌ G$
98		weeq1	$⊢ G = ⦋ ({H ↾}_{c}) / z ⦌ G \to (G We R_{1} (c) \leftrightarrow ⦋ ({H ↾}_{c}) / z ⦌ G We R_{1} (c))$
99	97 98	syl	$⊢ z = {H ↾}_{c} \to (G We R_{1} (c) \leftrightarrow ⦋ ({H ↾}_{c}) / z ⦌ G We R_{1} (c))$
100	96 99	sbciegf	$⊢ {H ↾}_{c} \in V \to (\underset{˙}{[} ({H ↾}_{c}) / z \underset{˙}{]} G We R_{1} (c) \leftrightarrow ⦋ ({H ↾}_{c}) / z ⦌ G We R_{1} (c))$
101	88 100	ax-mp	$⊢ \underset{˙}{[} ({H ↾}_{c}) / z \underset{˙}{]} G We R_{1} (c) \leftrightarrow ⦋ ({H ↾}_{c}) / z ⦌ G We R_{1} (c)$
102	93 101	sylib	$⊢ (c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \to ⦋ ({H ↾}_{c}) / z ⦌ G We R_{1} (c)$
103		recsval	$⊢ c \in On \to recs ((z \in V ⟼ G)) (c) = (z \in V ⟼ G) ({recs ((z \in V ⟼ G)) ↾}_{c})$
104	7	fveq1i	$⊢ H (c) = recs ((z \in V ⟼ G)) (c)$
105		fvex	$⊢ R_{1} (dom z) \in V$
106	105 105	xpex	$⊢ R_{1} (dom z) \times R_{1} (dom z) \in V$
107	106	inex2	$⊢ if (dom z = ⋃ dom z, F, E) \cap (R_{1} (dom z) \times R_{1} (dom z)) \in V$
108	6 107	eqeltri	$⊢ G \in V$
109	108	csbex	$⊢ ⦋ ({H ↾}_{c}) / z ⦌ G \in V$
110		eqid	$⊢ (z \in V ⟼ G) = (z \in V ⟼ G)$
111	110	fvmpts	$⊢ ({H ↾}_{c} \in V \land ⦋ ({H ↾}_{c}) / z ⦌ G \in V) \to (z \in V ⟼ G) ({H ↾}_{c}) = ⦋ ({H ↾}_{c}) / z ⦌ G$
112	88 109 111	mp2an	$⊢ (z \in V ⟼ G) ({H ↾}_{c}) = ⦋ ({H ↾}_{c}) / z ⦌ G$
113	7	reseq1i	$⊢ {H ↾}_{c} = {recs ((z \in V ⟼ G)) ↾}_{c}$
114	113	fveq2i	$⊢ (z \in V ⟼ G) ({H ↾}_{c}) = (z \in V ⟼ G) ({recs ((z \in V ⟼ G)) ↾}_{c})$
115	112 114	eqtr3i	$⊢ ⦋ ({H ↾}_{c}) / z ⦌ G = (z \in V ⟼ G) ({recs ((z \in V ⟼ G)) ↾}_{c})$
116	103 104 115	3eqtr4g	$⊢ c \in On \to H (c) = ⦋ ({H ↾}_{c}) / z ⦌ G$
117		weeq1	$⊢ H (c) = ⦋ ({H ↾}_{c}) / z ⦌ G \to (H (c) We R_{1} (c) \leftrightarrow ⦋ ({H ↾}_{c}) / z ⦌ G We R_{1} (c))$
118	116 117	syl	$⊢ c \in On \to (H (c) We R_{1} (c) \leftrightarrow ⦋ ({H ↾}_{c}) / z ⦌ G We R_{1} (c))$
119	118	3ad2ant1	$⊢ (c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \to (H (c) We R_{1} (c) \leftrightarrow ⦋ ({H ↾}_{c}) / z ⦌ G We R_{1} (c))$
120	102 119	mpbird	$⊢ (c \in On \land \forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \land (φ \land c \subseteq A)) \to H (c) We R_{1} (c)$
121	120	3exp	$⊢ c \in On \to (\forall d \in c ((φ \land d \subseteq A) \to H (d) We R_{1} (d)) \to ((φ \land c \subseteq A) \to H (c) We R_{1} (c)))$
122	17 23 121	tfis3	$⊢ A \in On \to ((φ \land A \subseteq A) \to H (A) We R_{1} (A))$
123	11 122	mpcom	$⊢ (φ \land A \subseteq A) \to H (A) We R_{1} (A)$
124	10 123	mpan2	$⊢ φ \to H (A) We R_{1} (A)$

Metamath Proof Explorer

Theorem aomclem6

Proof