brfi1indALT

Description: Alternate proof of brfi1ind , which does not use brfi1uzind . (Contributed by Alexander van der Vekens, 7-Jan-2018) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	brfi1ind.r	$⊢ Rel G$
	brfi1ind.f	$⊢ F \in V$
	brfi1ind.1	$⊢ (v = V \land e = E) \to (ψ \leftrightarrow φ)$
	brfi1ind.2	$⊢ (v = w \land e = f) \to (ψ \leftrightarrow θ)$
	brfi1ind.3	$⊢ (v G e \land n \in v) \to (v ∖ \{n\}) G F$
	brfi1ind.4	$⊢ (w = v ∖ \{n\} \land f = F) \to (θ \leftrightarrow χ)$
	brfi1ind.base	$⊢ (v G e \land \|v\| = 0) \to ψ$
	brfi1ind.step	$⊢ ((y + 1 \in ℕ_{0} \land (v G e \land \|v\| = y + 1 \land n \in v)) \land χ) \to ψ$
Assertion	brfi1indALT	$⊢ (V G E \land V \in Fin) \to φ$

Proof

Step	Hyp	Ref	Expression
1		brfi1ind.r	$⊢ Rel G$
2		brfi1ind.f	$⊢ F \in V$
3		brfi1ind.1	$⊢ (v = V \land e = E) \to (ψ \leftrightarrow φ)$
4		brfi1ind.2	$⊢ (v = w \land e = f) \to (ψ \leftrightarrow θ)$
5		brfi1ind.3	$⊢ (v G e \land n \in v) \to (v ∖ \{n\}) G F$
6		brfi1ind.4	$⊢ (w = v ∖ \{n\} \land f = F) \to (θ \leftrightarrow χ)$
7		brfi1ind.base	$⊢ (v G e \land \|v\| = 0) \to ψ$
8		brfi1ind.step	$⊢ ((y + 1 \in ℕ_{0} \land (v G e \land \|v\| = y + 1 \land n \in v)) \land χ) \to ψ$
9		hashcl	$⊢ V \in Fin \to \|V\| \in ℕ_{0}$
10		dfclel	$⊢ \|V\| \in ℕ_{0} \leftrightarrow \exists n (n = \|V\| \land n \in ℕ_{0})$
11		eqeq2	$⊢ x = 0 \to (\|v\| = x \leftrightarrow \|v\| = 0)$
12	11	anbi2d	$⊢ x = 0 \to ((v G e \land \|v\| = x) \leftrightarrow (v G e \land \|v\| = 0))$
13	12	imbi1d	$⊢ x = 0 \to (((v G e \land \|v\| = x) \to ψ) \leftrightarrow ((v G e \land \|v\| = 0) \to ψ))$
14	13	2albidv	$⊢ x = 0 \to (\forall v \forall e ((v G e \land \|v\| = x) \to ψ) \leftrightarrow \forall v \forall e ((v G e \land \|v\| = 0) \to ψ))$
15		eqeq2	$⊢ x = y \to (\|v\| = x \leftrightarrow \|v\| = y)$
16	15	anbi2d	$⊢ x = y \to ((v G e \land \|v\| = x) \leftrightarrow (v G e \land \|v\| = y))$
17	16	imbi1d	$⊢ x = y \to (((v G e \land \|v\| = x) \to ψ) \leftrightarrow ((v G e \land \|v\| = y) \to ψ))$
18	17	2albidv	$⊢ x = y \to (\forall v \forall e ((v G e \land \|v\| = x) \to ψ) \leftrightarrow \forall v \forall e ((v G e \land \|v\| = y) \to ψ))$
19		eqeq2	$⊢ x = y + 1 \to (\|v\| = x \leftrightarrow \|v\| = y + 1)$
20	19	anbi2d	$⊢ x = y + 1 \to ((v G e \land \|v\| = x) \leftrightarrow (v G e \land \|v\| = y + 1))$
21	20	imbi1d	$⊢ x = y + 1 \to (((v G e \land \|v\| = x) \to ψ) \leftrightarrow ((v G e \land \|v\| = y + 1) \to ψ))$
22	21	2albidv	$⊢ x = y + 1 \to (\forall v \forall e ((v G e \land \|v\| = x) \to ψ) \leftrightarrow \forall v \forall e ((v G e \land \|v\| = y + 1) \to ψ))$
23		eqeq2	$⊢ x = n \to (\|v\| = x \leftrightarrow \|v\| = n)$
24	23	anbi2d	$⊢ x = n \to ((v G e \land \|v\| = x) \leftrightarrow (v G e \land \|v\| = n))$
25	24	imbi1d	$⊢ x = n \to (((v G e \land \|v\| = x) \to ψ) \leftrightarrow ((v G e \land \|v\| = n) \to ψ))$
26	25	2albidv	$⊢ x = n \to (\forall v \forall e ((v G e \land \|v\| = x) \to ψ) \leftrightarrow \forall v \forall e ((v G e \land \|v\| = n) \to ψ))$
27	7	gen2	$⊢ \forall v \forall e ((v G e \land \|v\| = 0) \to ψ)$
28		breq12	$⊢ (v = w \land e = f) \to (v G e \leftrightarrow w G f)$
29		fveqeq2	$⊢ v = w \to (\|v\| = y \leftrightarrow \|w\| = y)$
30	29	adantr	$⊢ (v = w \land e = f) \to (\|v\| = y \leftrightarrow \|w\| = y)$
31	28 30	anbi12d	$⊢ (v = w \land e = f) \to ((v G e \land \|v\| = y) \leftrightarrow (w G f \land \|w\| = y))$
32	31 4	imbi12d	$⊢ (v = w \land e = f) \to (((v G e \land \|v\| = y) \to ψ) \leftrightarrow ((w G f \land \|w\| = y) \to θ))$
33	32	cbval2vw	$⊢ \forall v \forall e ((v G e \land \|v\| = y) \to ψ) \leftrightarrow \forall w \forall f ((w G f \land \|w\| = y) \to θ)$
34		nn0p1gt0	$⊢ y \in ℕ_{0} \to 0 < y + 1$
35	34	adantr	$⊢ (y \in ℕ_{0} \land \|v\| = y + 1) \to 0 < y + 1$
36		simpr	$⊢ (y \in ℕ_{0} \land \|v\| = y + 1) \to \|v\| = y + 1$
37	35 36	breqtrrd	$⊢ (y \in ℕ_{0} \land \|v\| = y + 1) \to 0 < \|v\|$
38	37	adantrl	$⊢ (y \in ℕ_{0} \land (v G e \land \|v\| = y + 1)) \to 0 < \|v\|$
39		hashgt0elex	$⊢ (v \in V \land 0 < \|v\|) \to \exists n n \in v$
40		vex	$⊢ v \in V$
41		simpr	$⊢ (y \in ℕ_{0} \land n \in v) \to n \in v$
42		simpl	$⊢ (y \in ℕ_{0} \land n \in v) \to y \in ℕ_{0}$
43		hashdifsnp1	$⊢ (v \in V \land n \in v \land y \in ℕ_{0}) \to (\|v\| = y + 1 \to \|v ∖ \{n\}\| = y)$
44	40 41 42 43	mp3an2i	$⊢ (y \in ℕ_{0} \land n \in v) \to (\|v\| = y + 1 \to \|v ∖ \{n\}\| = y)$
45	44	imp	$⊢ ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1) \to \|v ∖ \{n\}\| = y$
46		peano2nn0	$⊢ y \in ℕ_{0} \to y + 1 \in ℕ_{0}$
47	46	ad2antrr	$⊢ ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1) \to y + 1 \in ℕ_{0}$
48	47	ad2antlr	$⊢ (((\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \land ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1)) \land v G e) \to y + 1 \in ℕ_{0}$
49		simpr	$⊢ (((\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \land ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1)) \land v G e) \to v G e$
50		simplrr	$⊢ (((\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \land ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1)) \land v G e) \to \|v\| = y + 1$
51		simprlr	$⊢ ((\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \land ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1)) \to n \in v$
52	51	adantr	$⊢ (((\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \land ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1)) \land v G e) \to n \in v$
53	49 50 52	3jca	$⊢ (((\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \land ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1)) \land v G e) \to (v G e \land \|v\| = y + 1 \land n \in v)$
54	48 53	jca	$⊢ (((\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \land ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1)) \land v G e) \to (y + 1 \in ℕ_{0} \land (v G e \land \|v\| = y + 1 \land n \in v))$
55	40	difexi	$⊢ v ∖ \{n\} \in V$
56		breq12	$⊢ (w = v ∖ \{n\} \land f = F) \to (w G f \leftrightarrow (v ∖ \{n\}) G F)$
57		fveqeq2	$⊢ w = v ∖ \{n\} \to (\|w\| = y \leftrightarrow \|v ∖ \{n\}\| = y)$
58	57	adantr	$⊢ (w = v ∖ \{n\} \land f = F) \to (\|w\| = y \leftrightarrow \|v ∖ \{n\}\| = y)$
59	56 58	anbi12d	$⊢ (w = v ∖ \{n\} \land f = F) \to ((w G f \land \|w\| = y) \leftrightarrow ((v ∖ \{n\}) G F \land \|v ∖ \{n\}\| = y))$
60	59 6	imbi12d	$⊢ (w = v ∖ \{n\} \land f = F) \to (((w G f \land \|w\| = y) \to θ) \leftrightarrow (((v ∖ \{n\}) G F \land \|v ∖ \{n\}\| = y) \to χ))$
61	60	spc2gv	$⊢ (v ∖ \{n\} \in V \land F \in V) \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to (((v ∖ \{n\}) G F \land \|v ∖ \{n\}\| = y) \to χ))$
62	55 2 61	mp2an	$⊢ \forall w \forall f ((w G f \land \|w\| = y) \to θ) \to (((v ∖ \{n\}) G F \land \|v ∖ \{n\}\| = y) \to χ)$
63	62	expdimp	$⊢ (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \to (\|v ∖ \{n\}\| = y \to χ)$
64	63	ad2antrr	$⊢ (((\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \land ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1)) \land v G e) \to (\|v ∖ \{n\}\| = y \to χ)$
65	54 64 8	syl6an	$⊢ (((\forall w \forall f ((w G f \land \|w\| = y) \to θ) \land (v ∖ \{n\}) G F) \land ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1)) \land v G e) \to (\|v ∖ \{n\}\| = y \to ψ)$
66	65	exp41	$⊢ \forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ((v ∖ \{n\}) G F \to (((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1) \to (v G e \to (\|v ∖ \{n\}\| = y \to ψ))))$
67	66	com15	$⊢ \|v ∖ \{n\}\| = y \to ((v ∖ \{n\}) G F \to (((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1) \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
68	67	com23	$⊢ \|v ∖ \{n\}\| = y \to (((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1) \to ((v ∖ \{n\}) G F \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
69	45 68	mpcom	$⊢ ((y \in ℕ_{0} \land n \in v) \land \|v\| = y + 1) \to ((v ∖ \{n\}) G F \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ)))$
70	69	ex	$⊢ (y \in ℕ_{0} \land n \in v) \to (\|v\| = y + 1 \to ((v ∖ \{n\}) G F \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
71	70	com23	$⊢ (y \in ℕ_{0} \land n \in v) \to ((v ∖ \{n\}) G F \to (\|v\| = y + 1 \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
72	71	ex	$⊢ y \in ℕ_{0} \to (n \in v \to ((v ∖ \{n\}) G F \to (\|v\| = y + 1 \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ)))))$
73	72	com15	$⊢ v G e \to (n \in v \to ((v ∖ \{n\}) G F \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ)))))$
74	73	imp	$⊢ (v G e \land n \in v) \to ((v ∖ \{n\}) G F \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
75	5 74	mpd	$⊢ (v G e \land n \in v) \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ)))$
76	75	ex	$⊢ v G e \to (n \in v \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
77	76	com4l	$⊢ n \in v \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
78	77	exlimiv	$⊢ \exists n n \in v \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
79	39 78	syl	$⊢ (v \in V \land 0 < \|v\|) \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
80	79	ex	$⊢ v \in V \to (0 < \|v\| \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (v G e \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ)))))$
81	80	com25	$⊢ v \in V \to (v G e \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (0 < \|v\| \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ)))))$
82	81	elv	$⊢ v G e \to (\|v\| = y + 1 \to (y \in ℕ_{0} \to (0 < \|v\| \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))))$
83	82	imp	$⊢ (v G e \land \|v\| = y + 1) \to (y \in ℕ_{0} \to (0 < \|v\| \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ)))$
84	83	impcom	$⊢ (y \in ℕ_{0} \land (v G e \land \|v\| = y + 1)) \to (0 < \|v\| \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ))$
85	38 84	mpd	$⊢ (y \in ℕ_{0} \land (v G e \land \|v\| = y + 1)) \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to ψ)$
86	85	impancom	$⊢ (y \in ℕ_{0} \land \forall w \forall f ((w G f \land \|w\| = y) \to θ)) \to ((v G e \land \|v\| = y + 1) \to ψ)$
87	86	alrimivv	$⊢ (y \in ℕ_{0} \land \forall w \forall f ((w G f \land \|w\| = y) \to θ)) \to \forall v \forall e ((v G e \land \|v\| = y + 1) \to ψ)$
88	87	ex	$⊢ y \in ℕ_{0} \to (\forall w \forall f ((w G f \land \|w\| = y) \to θ) \to \forall v \forall e ((v G e \land \|v\| = y + 1) \to ψ))$
89	33 88	biimtrid	$⊢ y \in ℕ_{0} \to (\forall v \forall e ((v G e \land \|v\| = y) \to ψ) \to \forall v \forall e ((v G e \land \|v\| = y + 1) \to ψ))$
90	14 18 22 26 27 89	nn0ind	$⊢ n \in ℕ_{0} \to \forall v \forall e ((v G e \land \|v\| = n) \to ψ)$
91	1	brrelex12i	$⊢ V G E \to (V \in V \land E \in V)$
92		breq12	$⊢ (v = V \land e = E) \to (v G e \leftrightarrow V G E)$
93		fveqeq2	$⊢ v = V \to (\|v\| = n \leftrightarrow \|V\| = n)$
94	93	adantr	$⊢ (v = V \land e = E) \to (\|v\| = n \leftrightarrow \|V\| = n)$
95	92 94	anbi12d	$⊢ (v = V \land e = E) \to ((v G e \land \|v\| = n) \leftrightarrow (V G E \land \|V\| = n))$
96	95 3	imbi12d	$⊢ (v = V \land e = E) \to (((v G e \land \|v\| = n) \to ψ) \leftrightarrow ((V G E \land \|V\| = n) \to φ))$
97	96	spc2gv	$⊢ (V \in V \land E \in V) \to (\forall v \forall e ((v G e \land \|v\| = n) \to ψ) \to ((V G E \land \|V\| = n) \to φ))$
98	97	com23	$⊢ (V \in V \land E \in V) \to ((V G E \land \|V\| = n) \to (\forall v \forall e ((v G e \land \|v\| = n) \to ψ) \to φ))$
99	98	expd	$⊢ (V \in V \land E \in V) \to (V G E \to (\|V\| = n \to (\forall v \forall e ((v G e \land \|v\| = n) \to ψ) \to φ)))$
100	91 99	mpcom	$⊢ V G E \to (\|V\| = n \to (\forall v \forall e ((v G e \land \|v\| = n) \to ψ) \to φ))$
101	100	imp	$⊢ (V G E \land \|V\| = n) \to (\forall v \forall e ((v G e \land \|v\| = n) \to ψ) \to φ)$
102	90 101	syl5	$⊢ (V G E \land \|V\| = n) \to (n \in ℕ_{0} \to φ)$
103	102	expcom	$⊢ \|V\| = n \to (V G E \to (n \in ℕ_{0} \to φ))$
104	103	com23	$⊢ \|V\| = n \to (n \in ℕ_{0} \to (V G E \to φ))$
105	104	eqcoms	$⊢ n = \|V\| \to (n \in ℕ_{0} \to (V G E \to φ))$
106	105	imp	$⊢ (n = \|V\| \land n \in ℕ_{0}) \to (V G E \to φ)$
107	106	exlimiv	$⊢ \exists n (n = \|V\| \land n \in ℕ_{0}) \to (V G E \to φ)$
108	10 107	sylbi	$⊢ \|V\| \in ℕ_{0} \to (V G E \to φ)$
109	9 108	syl	$⊢ V \in Fin \to (V G E \to φ)$
110	109	impcom	$⊢ (V G E \land V \in Fin) \to φ$

Metamath Proof Explorer

Theorem brfi1indALT

Proof