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	syl6bi	$⊢ (χ \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		simpl	$⊢ (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 ↾}_{⋃ ⋃ R}) x$
66		df-br	$⊢ S ({I ↾}_{⋃ ⋃ R}) x \leftrightarrow ⟨S, x⟩ \in ({I ↾}_{⋃ ⋃ R})$
67	65 66	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, x⟩ \in ({I ↾}_{⋃ ⋃ R})$
68		vex	$⊢ x \in V$
69	68	opelresi	$⊢ ⟨S, x⟩ \in ({I ↾}_{⋃ ⋃ R}) \leftrightarrow (S \in ⋃ ⋃ R \land ⟨S, x⟩ \in I)$
70	67 69	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)$
71		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$
72		df-br	$⊢ S I x \leftrightarrow ⟨S, x⟩ \in I$
73	71 72	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$
74	68	ideq	$⊢ S I x \leftrightarrow S = x$
75	73 74	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$
76	70 75	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$
77		breq1	$⊢ S = x \to (S ({I ↾}_{⋃ ⋃ R}) x \leftrightarrow x ({I ↾}_{⋃ ⋃ R}) x)$
78		eqeq2	$⊢ S = x \to (i = S \leftrightarrow i = x)$
79	78	3anbi1d	$⊢ S = x \to ((i = S \land φ \land (η \land R \in V)) \leftrightarrow (i = x \land φ \land (η \land R \in V)))$
80	79	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)))$
81	80	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})))$
82	77 81	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}))))$
83		simprl	$⊢ ((η \land R \in V) \land (φ \land i = x)) \to φ$
84	4	ad2antll	$⊢ ((η \land R \in V) \land (φ \land i = x)) \to (φ \leftrightarrow ψ)$
85	83 84	mpbid	$⊢ ((η \land R \in V) \land (φ \land i = x)) \to ψ$
86	85	expcom	$⊢ (φ \land i = x) \to ((η \land R \in V) \to ψ)$
87	86	expcom	$⊢ i = x \to (φ \to ((η \land R \in V) \to ψ))$
88	87	3imp	$⊢ (i = x \land φ \land (η \land R \in V)) \to ψ$
89	88	exlimiv	$⊢ \exists i (i = x \land φ \land (η \land R \in V)) \to ψ$
90	89	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 ψ$
91	82 90	syl6bi	$⊢ 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 ψ)$
92	76 91	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 ψ$
93	92	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 ψ)$
94	64 93	mpancom	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to (S ({I ↾}_{⋃ ⋃ R}) x \to ψ)$
95		breq	$⊢ R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R} \to (S (R ↑_{r} 0) x \leftrightarrow S ({I ↾}_{⋃ ⋃ R}) x)$
96	95	imbi1d	$⊢ R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R} \to ((S (R ↑_{r} 0) x \to ψ) \leftrightarrow (S ({I ↾}_{⋃ ⋃ R}) x \to ψ))$
97	94 96	imbitrrid	$⊢ R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R} \to (((η \land R \in V) \land 0 \in ℕ_{0}) \to (S (R ↑_{r} 0) x \to ψ))$
98	39 97	mpcom	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to (S (R ↑_{r} 0) x \to ψ)$
99	98	alrimiv	$⊢ ((η \land R \in V) \land 0 \in ℕ_{0}) \to \forall x (S (R ↑_{r} 0) x \to ψ)$
100		breq2	$⊢ i = x \to (S (R ↑_{r} l) i \leftrightarrow S (R ↑_{r} l) x)$
101	100 4	imbi12d	$⊢ i = x \to ((S (R ↑_{r} l) i \to φ) \leftrightarrow (S (R ↑_{r} l) x \to ψ))$
102	101	cbvalvw	$⊢ \forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall x (S (R ↑_{r} l) x \to ψ)$
103	102	bicomi	$⊢ \forall x (S (R ↑_{r} l) x \to ψ) \leftrightarrow \forall i (S (R ↑_{r} l) i \to φ)$
104		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 φ)))$
105	104	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}))$
106	105	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})))$
107	106	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}))))$
108	1	adantr	$⊢ (η \land R \in V) \to Rel R$
109	108	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$
110		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}$
111	109 110	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)$
112		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$
113	2	adantr	$⊢ (η \land R \in V) \to S \in V$
114	113	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$
115		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))$
116	114 68 115	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))$
117	112 116	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)$
118		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)$
119		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}$
120	119	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}$
121		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 φ))$
122	121	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 φ))$
123	118 120 122	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 φ)$
124		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)$
125		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$
126	125	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$
127	126	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$
128		breq2	$⊢ i = j \to (S (R ↑_{r} l) i \leftrightarrow S (R ↑_{r} l) j)$
129	128 5	imbi12d	$⊢ i = j \to ((S (R ↑_{r} l) i \to φ) \leftrightarrow (S (R ↑_{r} l) j \to θ))$
130	129	cbvalvw	$⊢ \forall i (S (R ↑_{r} l) i \to φ) \leftrightarrow \forall j (S (R ↑_{r} l) j \to θ)$
131		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 θ))$
132		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 θ)))$
133	132	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))))$
134	133	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)))))$
135	134	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))))))$
136	135	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)))))))$
137	131 136	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))))))))$
138		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$
139	138	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$
140	139	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$
141		sp	$⊢ \forall j (S (R ↑_{r} l) j \to θ) \to (S (R ↑_{r} l) j \to θ)$
142	141	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 θ)$
143	140 142	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 θ$
144	137 143	syl6bi	$⊢ (\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 θ)$
145	130 144	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 θ$
146	7	adantr	$⊢ (η \land R \in V) \to (j R x \to (θ \to ψ))$
147	124 127 145 146	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 ψ$
148	123 147	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 ψ$
149	148	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 ψ)$
150	149	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 ψ))$
151	150	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 ψ)))$
152	151	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 ψ)))$
153	152	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 ψ))$
154	153	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 ψ))$
155	154	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 ψ)$
156	155	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 ψ)$
157	156	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 ψ$
158	157	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 ψ$
159	117 158	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 ψ$
160	159	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 ψ)$
161		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)$
162	161	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 ψ))$
163	160 162	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 ψ))$
164	111 163	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 ψ)$
165	164	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 ψ)$
166	107 165	syl6bi	$⊢ (\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 ψ))$
167	103 166	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 ψ)$
168	167	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 ψ)$
169	168	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 ψ))$
170	169	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 ψ)))$
171	14 21 28 35 99 170	nn0ind	$⊢ n \in ℕ_{0} \to (((η \land R \in V) \land n \in ℕ_{0}) \to \forall x (S (R ↑_{r} n) x \to ψ))$
172	171	anabsi7	$⊢ ((η \land R \in V) \land n \in ℕ_{0}) \to \forall x (S (R ↑_{r} n) x \to ψ)$
173	172	19.21bi	$⊢ ((η \land R \in V) \land n \in ℕ_{0}) \to (S (R ↑_{r} n) x \to ψ)$
174	173	exp31	$⊢ η \to (R \in V \to (n \in ℕ_{0} \to (S (R ↑_{r} n) x \to ψ)))$
175		reldmrelexp	$⊢ Rel dom ↑_{r}$
176	175	ovprc1	$⊢ \neg R \in V \to R ↑_{r} n = \emptyset$
177	176	breqd	$⊢ \neg R \in V \to (S (R ↑_{r} n) x \leftrightarrow S \emptyset x)$
178		br0	$⊢ \neg S \emptyset x$
179	178	pm2.21i	$⊢ S \emptyset x \to ψ$
180	177 179	syl6bi	$⊢ \neg R \in V \to (S (R ↑_{r} n) x \to ψ)$
181	180	a1d	$⊢ \neg R \in V \to (n \in ℕ_{0} \to (S (R ↑_{r} n) x \to ψ))$
182	174 181	pm2.61d1	$⊢ η \to (n \in ℕ_{0} \to (S (R ↑_{r} n) x \to ψ))$

Metamath Proof Explorer

Theorem relexpindlem

Proof