relexpindlem

Description: Principle of transitive induction, finite and non-class version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Proof shortened by Peter Mazsa, 2-Oct-2022) (Revised by AV, 13-Jul-2024)

	Ref	Expression
Hypotheses	relexpindlem.1	$⊢ η \to Rel R$
	relexpindlem.2	$⊢ η \to S \in V$
	relexpindlem.3	$⊢ i = S \to (φ \leftrightarrow χ)$
	relexpindlem.4	$⊢ i = x \to (φ \leftrightarrow ψ)$
	relexpindlem.5	$⊢ i = j \to (φ \leftrightarrow θ)$
	relexpindlem.6	$⊢ η \to χ$
	relexpindlem.7	$⊢ η \to (j R x \to (θ \to ψ))$
Assertion	relexpindlem	$⊢ η \to (n \in ℕ_{0} \to (S (R ↑_{r} n) x \to ψ))$

Proof

Step	Hyp	Ref	Expression
1		relexpindlem.1	$⊢ η \to Rel R$
2		relexpindlem.2	$⊢ η \to S \in V$
3		relexpindlem.3	$⊢ i = S \to (φ \leftrightarrow χ)$
4		relexpindlem.4	$⊢ i = x \to (φ \leftrightarrow ψ)$
5		relexpindlem.5	$⊢ i = j \to (φ \leftrightarrow θ)$
6		relexpindlem.6	$⊢ η \to χ$
7		relexpindlem.7	$⊢ η \to (j R x \to (θ \to ψ))$
8		eleq1	$⊢ k = 0 \to (k \in ℕ_{0} \leftrightarrow 0 \in ℕ_{0})$
9	8	anbi2d	$⊢ k = 0 \to (((η \land R \in V) \land k \in ℕ_{0}) \leftrightarrow ((η \land R \in V) \land 0 \in ℕ_{0}))$
10		oveq2	$⊢ k = 0 \to R ↑_{r} k = R ↑_{r} 0$
11	10	breqd	$⊢ k = 0 \to (S (R ↑_{r} k) x \leftrightarrow S (R ↑_{r} 0) x)$
12	11	imbi1d	$⊢ k = 0 \to ((S (R ↑_{r} k) x \to ψ) \leftrightarrow (S (R ↑_{r} 0) x \to ψ))$
13	12	albidv	$⊢ k = 0 \to (\forall x (S (R ↑_{r} k) x \to ψ) \leftrightarrow \forall x (S (R ↑_{r} 0) x \to ψ))$
14	9 13	imbi12d	$⊢ k = 0 \to ((((η \land R \in V) \land k \in ℕ_{0}) \to \forall x (S (R ↑_{r} k) x \to ψ)) \leftrightarrow (((η \land R \in V) \land 0 \in ℕ_{0}) \to \forall x (S (R ↑_{r} 0) x \to ψ)))$
15		eleq1	$⊢ k = l \to (k \in ℕ_{0} \leftrightarrow l \in ℕ_{0})$
16	15	anbi2d	$⊢ k = l \to (((η \land R \in V) \land k \in ℕ_{0}) \leftrightarrow ((η \land R \in V) \land l \in ℕ_{0}))$
17		oveq2	$⊢ k = l \to R ↑_{r} k = R ↑_{r} l$
18	17	breqd	$⊢ k = l \to (S (R ↑_{r} k) x \leftrightarrow S (R ↑_{r} l) x)$
19	18	imbi1d	$⊢ k = l \to ((S (R ↑_{r} k) x \to ψ) \leftrightarrow (S (R ↑_{r} l) x \to ψ))$
20	19	albidv	$⊢ k = l \to (\forall x (S (R ↑_{r} k) x \to ψ) \leftrightarrow \forall x (S (R ↑_{r} l) x \to ψ))$
21	16 20	imbi12d	$⊢ k = l \to ((((η \land R \in V) \land k \in ℕ_{0}) \to \forall x (S (R ↑_{r} k) x \to ψ)) \leftrightarrow (((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)))$
22		eleq1	$⊢ k = l + 1 \to (k \in ℕ_{0} \leftrightarrow l + 1 \in ℕ_{0})$
23	22	anbi2d	$⊢ k = l + 1 \to (((η \land R \in V) \land k \in ℕ_{0}) \leftrightarrow ((η \land R \in V) \land l + 1 \in ℕ_{0}))$
24		oveq2	$⊢ k = l + 1 \to R ↑_{r} k = R ↑_{r} (l + 1)$
25	24	breqd	$⊢ k = l + 1 \to (S (R ↑_{r} k) x \leftrightarrow S (R ↑_{r} (l + 1)) x)$
26	25	imbi1d	$⊢ k = l + 1 \to ((S (R ↑_{r} k) x \to ψ) \leftrightarrow (S (R ↑_{r} (l + 1)) x \to ψ))$
27	26	albidv	$⊢ k = l + 1 \to (\forall x (S (R ↑_{r} k) x \to ψ) \leftrightarrow \forall x (S (R ↑_{r} (l + 1)) x \to ψ))$
28	23 27	imbi12d	$⊢ k = l + 1 \to ((((η \land R \in V) \land k \in ℕ_{0}) \to \forall x (S (R ↑_{r} k) x \to ψ)) \leftrightarrow (((η \land R \in V) \land l + 1 \in ℕ_{0}) \to \forall x (S (R ↑_{r} (l + 1)) x \to ψ)))$
29		eleq1	$⊢ k = n \to (k \in ℕ_{0} \leftrightarrow n \in ℕ_{0})$
30	29	anbi2d	$⊢ k = n \to (((η \land R \in V) \land k \in ℕ_{0}) \leftrightarrow ((η \land R \in V) \land n \in ℕ_{0}))$
31		oveq2	$⊢ k = n \to R ↑_{r} k = R ↑_{r} n$
32	31	breqd	$⊢ k = n \to (S (R ↑_{r} k) x \leftrightarrow S (R ↑_{r} n) x)$
33	32	imbi1d	$⊢ k = n \to ((S (R ↑_{r} k) x \to ψ) \leftrightarrow (S (R ↑_{r} n) x \to ψ))$
34	33	albidv	$⊢ k = n \to (\forall x (S (R ↑_{r} k) x \to ψ) \leftrightarrow \forall x (S (R ↑_{r} n) x \to ψ))$
35	30 34	imbi12d	$⊢ k = n \to ((((η \land R \in V) \land k \in ℕ_{0}) \to \forall x (S (R ↑_{r} k) x \to ψ)) \leftrightarrow (((η \land R \in V) \land n \in ℕ_{0}) \to \forall x (S (R ↑_{r} n) x \to ψ)))$
36	1	anim1ci	$⊢ (η \land R \in V) \to (R \in V \land Rel R)$
37	36	adantr	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to (R \in V \land Rel R)$
38		relexp0	$⊢ (R \in V \land Rel R) \to R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R}$
39	37 38	syl	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R}$
40	6	adantr	$⊢ (η \land R \in V) \to χ$
41		simpl	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to (η \land R \in V)$
42	2	ad2antrl	$⊢ (χ \land (η \land R \in V)) \to S \in V$
43		simprl	$⊢ (i = S \land ((η \land R \in V) \land (φ \land i = S))) \to (η \land R \in V)$
44	43 40	jccil	$⊢ (i = S \land ((η \land R \in V) \land (φ \land i = S))) \to (χ \land (η \land R \in V))$
45	44	expcom	$⊢ ((η \land R \in V) \land (φ \land i = S)) \to (i = S \to (χ \land (η \land R \in V)))$
46	45	expcom	$⊢ (φ \land i = S) \to ((η \land R \in V) \to (i = S \to (χ \land (η \land R \in V))))$
47	46	expcom	$⊢ i = S \to (φ \to ((η \land R \in V) \to (i = S \to (χ \land (η \land R \in V)))))$
48	47	3imp1	$⊢ ((i = S \land φ \land (η \land R \in V)) \land i = S) \to (χ \land (η \land R \in V))$
49	48	expcom	$⊢ i = S \to ((i = S \land φ \land (η \land R \in V)) \to (χ \land (η \land R \in V)))$
50		simprr	$⊢ (χ \land ((η \land R \in V) \land i = S)) \to i = S$
51	3	ad2antll	$⊢ (χ \land ((η \land R \in V) \land i = S)) \to (φ \leftrightarrow χ)$
52	51	bicomd	$⊢ (χ \land ((η \land R \in V) \land i = S)) \to (χ \leftrightarrow φ)$
53		anbi1	$⊢ (χ \leftrightarrow φ) \to ((χ \land ((η \land R \in V) \land i = S)) \leftrightarrow (φ \land ((η \land R \in V) \land i = S)))$
54		simpl	$⊢ (φ \land ((η \land R \in V) \land i = S)) \to φ$
55	53 54	biimtrdi	$⊢ (χ \leftrightarrow φ) \to ((χ \land ((η \land R \in V) \land i = S)) \to φ)$
56	52 55	mpcom	$⊢ (χ \land ((η \land R \in V) \land i = S)) \to φ$
57		simprl	$⊢ (χ \land ((η \land R \in V) \land i = S)) \to (η \land R \in V)$
58	50 56 57	3jca	$⊢ (χ \land ((η \land R \in V) \land i = S)) \to (i = S \land φ \land (η \land R \in V))$
59	58	anassrs	$⊢ ((χ \land (η \land R \in V)) \land i = S) \to (i = S \land φ \land (η \land R \in V))$
60	59	expcom	$⊢ i = S \to ((χ \land (η \land R \in V)) \to (i = S \land φ \land (η \land R \in V)))$
61	49 60	impbid	$⊢ i = S \to ((i = S \land φ \land (η \land R \in V)) \leftrightarrow (χ \land (η \land R \in V)))$
62	61	spcegv	$⊢ S \in V \to ((χ \land (η \land R \in V)) \to \exists i (i = S \land φ \land (η \land R \in V)))$
63	42 62	mpcom	$⊢ (χ \land (η \land R \in V)) \to \exists i (i = S \land φ \land (η \land R \in V))$
64	40 41 63	syl2an2r	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to \exists i (i = S \land φ \land (η \land R \in V))$
65		df-br	$⊢ S ({I ↾}_{⋃ ⋃ R}) x \leftrightarrow ⟨S, x⟩ \in ({I ↾}_{⋃ ⋃ R})$
66	65	birani	$⊢ (S ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0}))) \to ⟨S, x⟩ \in ({I ↾}_{⋃ ⋃ R})$
67		vex	$⊢ x \in V$
68	67	opelresi	$⊢ ⟨S, x⟩ \in ({I ↾}_{⋃ ⋃ R}) \leftrightarrow (S \in ⋃ ⋃ R \land ⟨S, x⟩ \in I)$
69	66 68	sylib	$⊢ (S ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0}))) \to (S \in ⋃ ⋃ R \land ⟨S, x⟩ \in I)$
70		simplr	$⊢ ((S \in ⋃ ⋃ R \land ⟨S, x⟩ \in I) \land (S ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0})))) \to ⟨S, x⟩ \in I$
71		df-br	$⊢ S I x \leftrightarrow ⟨S, x⟩ \in I$
72	70 71	sylibr	$⊢ ((S \in ⋃ ⋃ R \land ⟨S, x⟩ \in I) \land (S ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0})))) \to S I x$
73	67	ideq	$⊢ S I x \leftrightarrow S = x$
74	72 73	sylib	$⊢ ((S \in ⋃ ⋃ R \land ⟨S, x⟩ \in I) \land (S ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0})))) \to S = x$
75	69 74	mpancom	$⊢ (S ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0}))) \to S = x$
76		breq1	$⊢ S = x \to (S ({I ↾}_{⋃ ⋃ R}) x \leftrightarrow x ({I ↾}_{⋃ ⋃ R}) x)$
77		eqeq2	$⊢ S = x \to (i = S \leftrightarrow i = x)$
78	77	3anbi1d	$⊢ S = x \to ((i = S \land φ \land (η \land R \in V)) \leftrightarrow (i = x \land φ \land (η \land R \in V)))$
79	78	exbidv	$⊢ S = x \to (\exists i (i = S \land φ \land (η \land R \in V)) \leftrightarrow \exists i (i = x \land φ \land (η \land R \in V)))$
80	79	anbi1d	$⊢ S = x \to ((\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0})) \leftrightarrow (\exists i (i = x \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0})))$
81	76 80	anbi12d	$⊢ S = x \to ((S ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0}))) \leftrightarrow (x ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = x \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0}))))$
82		simprl	$⊢ ((η \land R \in V) \land (φ \land i = x)) \to φ$
83	4	ad2antll	$⊢ ((η \land R \in V) \land (φ \land i = x)) \to (φ \leftrightarrow ψ)$
84	82 83	mpbid	$⊢ ((η \land R \in V) \land (φ \land i = x)) \to ψ$
85	84	expcom	$⊢ (φ \land i = x) \to ((η \land R \in V) \to ψ)$
86	85	expcom	$⊢ i = x \to (φ \to ((η \land R \in V) \to ψ))$
87	86	3imp	$⊢ (i = x \land φ \land (η \land R \in V)) \to ψ$
88	87	exlimiv	$⊢ \exists i (i = x \land φ \land (η \land R \in V)) \to ψ$
89	88	ad2antrl	$⊢ (x ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = x \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0}))) \to ψ$
90	81 89	biimtrdi	$⊢ S = x \to ((S ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0}))) \to ψ)$
91	75 90	mpcom	$⊢ (S ({I ↾}_{⋃ ⋃ R}) x \land (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0}))) \to ψ$
92	91	expcom	$⊢ (\exists i (i = S \land φ \land (η \land R \in V)) \land ((η \land R \in V) \land 0 \in ℕ_{0})) \to (S ({I ↾}_{⋃ ⋃ R}) x \to ψ)$
93	64 92	mpancom	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to (S ({I ↾}_{⋃ ⋃ R}) x \to ψ)$
94		breq	$⊢ R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R} \to (S (R ↑_{r} 0) x \leftrightarrow S ({I ↾}_{⋃ ⋃ R}) x)$
95	94	imbi1d	$⊢ R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R} \to ((S (R ↑_{r} 0) x \to ψ) \leftrightarrow (S ({I ↾}_{⋃ ⋃ R}) x \to ψ))$
96	93 95	imbitrrid	$⊢ R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R} \to (((η \land R \in V) \land 0 \in ℕ_{0}) \to (S (R ↑_{r} 0) x \to ψ))$
97	39 96	mpcom	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to (S (R ↑_{r} 0) x \to ψ)$
98	97	alrimiv	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to \forall x (S (R ↑_{r} 0) x \to ψ)$
99		breq2	$⊢ i = x \to (S (R ↑_{r} l) i \leftrightarrow S (R ↑_{r} l) x)$
100	99 4	imbi12d	$⊢ i = x \to ((S (R ↑_{r} l) i \to φ) \leftrightarrow (S (R ↑_{r} l) x \to ψ))$
101	100	cbvalvw	$⊢ \forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall x (S (R ↑_{r} l) x \to ψ)$
102	101	bicomi	$⊢ \forall x (S (R ↑_{r} l) x \to ψ) \leftrightarrow \forall i (S (R ↑_{r} l) i \to φ)$
103		imbi2	$⊢ (\forall x (S (R ↑_{r} l) x \to ψ) \leftrightarrow \forall i (S (R ↑_{r} l) i \to φ)) \to ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)) \leftrightarrow (((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)))$
104	103	anbi1d	$⊢ (\forall x (S (R ↑_{r} l) x \to ψ) \leftrightarrow \forall i (S (R ↑_{r} l) i \to φ)) \to (((((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)) \land l \in ℕ_{0}) \leftrightarrow ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))$
105	104	anbi2d	$⊢ (\forall x (S (R ↑_{r} l) x \to ψ) \leftrightarrow \forall i (S (R ↑_{r} l) i \to φ)) \to ((l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)) \land l \in ℕ_{0})) \leftrightarrow (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0})))$
106	105	anbi2d	$⊢ (\forall x (S (R ↑_{r} l) x \to ψ) \leftrightarrow \forall i (S (R ↑_{r} l) i \to φ)) \to (((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)) \land l \in ℕ_{0}))) \leftrightarrow ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))))$
107	1	adantr	$⊢ (η \land R \in V) \to Rel R$
108	107	adantr	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))) \to Rel R$
109		simprrr	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))) \to l \in ℕ_{0}$
110	108 109	relexpsucld	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))) \to R ↑_{r} (l + 1) = R \circ (R ↑_{r} l)$
111		simpl	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0})))) \to S (R \circ (R ↑_{r} l)) x$
112	2	adantr	$⊢ (η \land R \in V) \to S \in V$
113	112	ad2antrl	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0})))) \to S \in V$
114		brcog	$⊢ (S \in V \land x \in V) \to (S (R \circ (R ↑_{r} l)) x \leftrightarrow \exists j (S (R ↑_{r} l) j \land j R x))$
115	113 67 114	sylancl	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0})))) \to (S (R \circ (R ↑_{r} l)) x \leftrightarrow \exists j (S (R ↑_{r} l) j \land j R x))$
116	111 115	mpbid	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0})))) \to \exists j (S (R ↑_{r} l) j \land j R x)$
117		simprl	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))))) \to (η \land R \in V)$
118		simprrl	$⊢ (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))) \to l \in ℕ_{0}$
119	118	ad2antll	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))))) \to l \in ℕ_{0}$
120		simprl	$⊢ (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))) \to (((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ))$
121	120	ad2antll	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))))) \to (((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ))$
122	117 119 121	mp2and	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))))) \to \forall i (S (R ↑_{r} l) i \to φ)$
123		simprrl	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))) \to (η \land R \in V)$
124		simprrr	$⊢ ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))) \to j R x$
125	124	ad2antll	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))) \to j R x$
126	125	ad2antll	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))) \to j R x$
127		breq2	$⊢ i = j \to (S (R ↑_{r} l) i \leftrightarrow S (R ↑_{r} l) j)$
128	127 5	imbi12d	$⊢ i = j \to ((S (R ↑_{r} l) i \to φ) \leftrightarrow (S (R ↑_{r} l) j \to θ))$
129	128	cbvalvw	$⊢ \forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)$
130		id	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)) \to (\forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ))$
131		imbi2	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)) \to ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \leftrightarrow (((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)))$
132	131	anbi1d	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)) \to (((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))) \leftrightarrow ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))$
133	132	anbi2d	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)) \to ((l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))) \leftrightarrow (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))))$
134	133	anbi2d	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)) \to (((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))) \leftrightarrow ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))$
135	134	anbi2d	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)) \to ((S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))))) \leftrightarrow (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))))))$
136	130 135	anbi12d	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)) \to ((\forall i (S (R ↑_{r} l) i \to φ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))) \leftrightarrow (\forall j (S (R ↑_{r} l) j \to θ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))))$
137		simprrl	$⊢ ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))) \to S (R ↑_{r} l) j$
138	137	ad2antll	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))) \to S (R ↑_{r} l) j$
139	138	ad2antll	$⊢ (\forall j (S (R ↑_{r} l) j \to θ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))) \to S (R ↑_{r} l) j$
140		sp	$⊢ \forall j (S (R ↑_{r} l) j \to θ) \to (S (R ↑_{r} l) j \to θ)$
141	140	adantr	$⊢ (\forall j (S (R ↑_{r} l) j \to θ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))) \to (S (R ↑_{r} l) j \to θ)$
142	139 141	mpd	$⊢ (\forall j (S (R ↑_{r} l) j \to θ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall j (S (R ↑_{r} l) j \to θ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))) \to θ$
143	136 142	biimtrdi	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)) \to ((\forall i (S (R ↑_{r} l) i \to φ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))) \to θ)$
144	129 143	ax-mp	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))) \to θ$
145	7	adantr	$⊢ (η \land R \in V) \to (j R x \to (θ \to ψ))$
146	123 126 144 145	syl3c	$⊢ (\forall i (S (R ↑_{r} l) i \to φ) \land (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))))) \to ψ$
147	122 146	mpancom	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))))) \to ψ$
148	147	expcom	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))))) \to (S (R \circ (R ↑_{r} l)) x \to ψ)$
149	148	expcom	$⊢ (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x)))) \to ((η \land R \in V) \to (S (R \circ (R ↑_{r} l)) x \to ψ))$
150	149	expcom	$⊢ ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land (l \in ℕ_{0} \land (S (R ↑_{r} l) j \land j R x))) \to (l + 1 \in ℕ_{0} \to ((η \land R \in V) \to (S (R \circ (R ↑_{r} l)) x \to ψ)))$
151	150	anassrs	$⊢ (((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}) \land (S (R ↑_{r} l) j \land j R x)) \to (l + 1 \in ℕ_{0} \to ((η \land R \in V) \to (S (R \circ (R ↑_{r} l)) x \to ψ)))$
152	151	impcom	$⊢ (l + 1 \in ℕ_{0} \land (((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}) \land (S (R ↑_{r} l) j \land j R x))) \to ((η \land R \in V) \to (S (R \circ (R ↑_{r} l)) x \to ψ))$
153	152	anassrs	$⊢ ((l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0})) \land (S (R ↑_{r} l) j \land j R x)) \to ((η \land R \in V) \to (S (R \circ (R ↑_{r} l)) x \to ψ))$
154	153	impcom	$⊢ ((η \land R \in V) \land ((l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0})) \land (S (R ↑_{r} l) j \land j R x))) \to (S (R \circ (R ↑_{r} l)) x \to ψ)$
155	154	anassrs	$⊢ (((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))) \land (S (R ↑_{r} l) j \land j R x)) \to (S (R \circ (R ↑_{r} l)) x \to ψ)$
156	155	impcom	$⊢ (S (R \circ (R ↑_{r} l)) x \land (((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))) \land (S (R ↑_{r} l) j \land j R x))) \to ψ$
157	156	anassrs	$⊢ ((S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0})))) \land (S (R ↑_{r} l) j \land j R x)) \to ψ$
158	116 157	exlimddv	$⊢ (S (R \circ (R ↑_{r} l)) x \land ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0})))) \to ψ$
159	158	expcom	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))) \to (S (R \circ (R ↑_{r} l)) x \to ψ)$
160		breq	$⊢ R ↑_{r} (l + 1) = R \circ (R ↑_{r} l) \to (S (R ↑_{r} (l + 1)) x \leftrightarrow S (R \circ (R ↑_{r} l)) x)$
161	160	imbi1d	$⊢ R ↑_{r} (l + 1) = R \circ (R ↑_{r} l) \to ((S (R ↑_{r} (l + 1)) x \to ψ) \leftrightarrow (S (R \circ (R ↑_{r} l)) x \to ψ))$
162	159 161	imbitrrid	$⊢ R ↑_{r} (l + 1) = R \circ (R ↑_{r} l) \to (((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))) \to (S (R ↑_{r} (l + 1)) x \to ψ))$
163	110 162	mpcom	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))) \to (S (R ↑_{r} (l + 1)) x \to ψ)$
164	163	alrimiv	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall i (S (R ↑_{r} l) i \to φ)) \land l \in ℕ_{0}))) \to \forall x (S (R ↑_{r} (l + 1)) x \to ψ)$
165	106 164	biimtrdi	$⊢ (\forall x (S (R ↑_{r} l) x \to ψ) \leftrightarrow \forall i (S (R ↑_{r} l) i \to φ)) \to (((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)) \land l \in ℕ_{0}))) \to \forall x (S (R ↑_{r} (l + 1)) x \to ψ))$
166	102 165	ax-mp	$⊢ ((η \land R \in V) \land (l + 1 \in ℕ_{0} \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)) \land l \in ℕ_{0}))) \to \forall x (S (R ↑_{r} (l + 1)) x \to ψ)$
167	166	anassrs	$⊢ (((η \land R \in V) \land l + 1 \in ℕ_{0}) \land ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)) \land l \in ℕ_{0})) \to \forall x (S (R ↑_{r} (l + 1)) x \to ψ)$
168	167	expcom	$⊢ ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)) \land l \in ℕ_{0}) \to (((η \land R \in V) \land l + 1 \in ℕ_{0}) \to \forall x (S (R ↑_{r} (l + 1)) x \to ψ))$
169	168	expcom	$⊢ l \in ℕ_{0} \to ((((η \land R \in V) \land l \in ℕ_{0}) \to \forall x (S (R ↑_{r} l) x \to ψ)) \to (((η \land R \in V) \land l + 1 \in ℕ_{0}) \to \forall x (S (R ↑_{r} (l + 1)) x \to ψ)))$
170	14 21 28 35 98 169	nn0ind	$⊢ n \in ℕ_{0} \to (((η \land R \in V) \land n \in ℕ_{0}) \to \forall x (S (R ↑_{r} n) x \to ψ))$
171	170	anabsi7	$⊢ ((η \land R \in V) \land n \in ℕ_{0}) \to \forall x (S (R ↑_{r} n) x \to ψ)$
172	171	19.21bi	$⊢ ((η \land R \in V) \land n \in ℕ_{0}) \to (S (R ↑_{r} n) x \to ψ)$
173	172	exp31	$⊢ η \to (R \in V \to (n \in ℕ_{0} \to (S (R ↑_{r} n) x \to ψ)))$
174		reldmrelexp	$⊢ Rel dom ↑_{r}$
175	174	ovprc1	$⊢ \neg R \in V \to R ↑_{r} n = \emptyset$
176	175	breqd	$⊢ \neg R \in V \to (S (R ↑_{r} n) x \leftrightarrow S \emptyset x)$
177		br0	$⊢ \neg S \emptyset x$
178	177	pm2.21i	$⊢ S \emptyset x \to ψ$
179	176 178	biimtrdi	$⊢ \neg R \in V \to (S (R ↑_{r} n) x \to ψ)$
180	179	a1d	$⊢ \neg R \in V \to (n \in ℕ_{0} \to (S (R ↑_{r} n) x \to ψ))$
181	173 180	pm2.61d1	$⊢ η \to (n \in ℕ_{0} \to (S (R ↑_{r} n) x \to ψ))$

Metamath Proof Explorer

Theorem relexpindlem

Proof