fmla1

Description: The valid Godel formulas of height 1 is the set of all formulas of the form ( a |g b ) and A.g k a with atoms a , b of the form x e. y . (Contributed by AV, 20-Sep-2023)

		Ref	Expression
	Assertion	fmla1	\|- ( Fmla ` 1o ) = ( ( { (/) } X. ( _om X. _om ) ) u. { x \| E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) } )

Proof

Step	Hyp	Ref	Expression
1		df-1o	\|- 1o = suc (/)
2	1	fveq2i	\|- ( Fmla ` 1o ) = ( Fmla ` suc (/) )
3		peano1	\|- (/) e. _om
4		fmlasuc	\|- ( (/) e. _om -> ( Fmla ` suc (/) ) = ( ( Fmla ` (/) ) u. { x \| E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) } ) )
5	3 4	ax-mp	\|- ( Fmla ` suc (/) ) = ( ( Fmla ` (/) ) u. { x \| E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) } )
6		fmla0xp	\|- ( Fmla ` (/) ) = ( { (/) } X. ( _om X. _om ) )
7		fmla0	\|- ( Fmla ` (/) ) = { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) }
8	7	rexeqi	\|- ( E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) <-> E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) )
9		eqeq1	\|- ( y = p -> ( y = ( i e.g j ) <-> p = ( i e.g j ) ) )
10	9	2rexbidv	\|- ( y = p -> ( E. i e. _om E. j e. _om y = ( i e.g j ) <-> E. i e. _om E. j e. _om p = ( i e.g j ) ) )
11	10	elrab	\|- ( p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } <-> ( p e. _V /\ E. i e. _om E. j e. _om p = ( i e.g j ) ) )
12		oveq1	\|- ( p = ( i e.g j ) -> ( p \|g q ) = ( ( i e.g j ) \|g q ) )
13	12	eqeq2d	\|- ( p = ( i e.g j ) -> ( x = ( p \|g q ) <-> x = ( ( i e.g j ) \|g q ) ) )
14	13	rexbidv	\|- ( p = ( i e.g j ) -> ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) <-> E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) \|g q ) ) )
15		eqidd	\|- ( p = ( i e.g j ) -> k = k )
16		id	\|- ( p = ( i e.g j ) -> p = ( i e.g j ) )
17	15 16	goaleq12d	\|- ( p = ( i e.g j ) -> A.g k p = A.g k ( i e.g j ) )
18	17	eqeq2d	\|- ( p = ( i e.g j ) -> ( x = A.g k p <-> x = A.g k ( i e.g j ) ) )
19	18	rexbidv	\|- ( p = ( i e.g j ) -> ( E. k e. _om x = A.g k p <-> E. k e. _om x = A.g k ( i e.g j ) ) )
20	14 19	orbi12d	\|- ( p = ( i e.g j ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) <-> ( E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) \|g q ) \/ E. k e. _om x = A.g k ( i e.g j ) ) ) )
21		eqeq1	\|- ( z = q -> ( z = ( k e.g l ) <-> q = ( k e.g l ) ) )
22	21	2rexbidv	\|- ( z = q -> ( E. k e. _om E. l e. _om z = ( k e.g l ) <-> E. k e. _om E. l e. _om q = ( k e.g l ) ) )
23		fmla0	\|- ( Fmla ` (/) ) = { z e. _V \| E. k e. _om E. l e. _om z = ( k e.g l ) }
24	22 23	elrab2	\|- ( q e. ( Fmla ` (/) ) <-> ( q e. _V /\ E. k e. _om E. l e. _om q = ( k e.g l ) ) )
25		oveq2	\|- ( q = ( k e.g l ) -> ( ( i e.g j ) \|g q ) = ( ( i e.g j ) \|g ( k e.g l ) ) )
26	25	eqeq2d	\|- ( q = ( k e.g l ) -> ( x = ( ( i e.g j ) \|g q ) <-> x = ( ( i e.g j ) \|g ( k e.g l ) ) ) )
27	26	biimpcd	\|- ( x = ( ( i e.g j ) \|g q ) -> ( q = ( k e.g l ) -> x = ( ( i e.g j ) \|g ( k e.g l ) ) ) )
28	27	reximdv	\|- ( x = ( ( i e.g j ) \|g q ) -> ( E. l e. _om q = ( k e.g l ) -> E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) ) )
29	28	reximdv	\|- ( x = ( ( i e.g j ) \|g q ) -> ( E. k e. _om E. l e. _om q = ( k e.g l ) -> E. k e. _om E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) ) )
30	29	com12	\|- ( E. k e. _om E. l e. _om q = ( k e.g l ) -> ( x = ( ( i e.g j ) \|g q ) -> E. k e. _om E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) ) )
31	24 30	simplbiim	\|- ( q e. ( Fmla ` (/) ) -> ( x = ( ( i e.g j ) \|g q ) -> E. k e. _om E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) ) )
32	31	rexlimiv	\|- ( E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) \|g q ) -> E. k e. _om E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) )
33	32	orim1i	\|- ( ( E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) \|g q ) \/ E. k e. _om x = A.g k ( i e.g j ) ) -> ( E. k e. _om E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ E. k e. _om x = A.g k ( i e.g j ) ) )
34		r19.43	\|- ( E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) <-> ( E. k e. _om E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ E. k e. _om x = A.g k ( i e.g j ) ) )
35	33 34	sylibr	\|- ( ( E. q e. ( Fmla ` (/) ) x = ( ( i e.g j ) \|g q ) \/ E. k e. _om x = A.g k ( i e.g j ) ) -> E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) )
36	20 35	biimtrdi	\|- ( p = ( i e.g j ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) -> E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
37	36	com12	\|- ( ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) -> ( p = ( i e.g j ) -> E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
38	37	reximdv	\|- ( ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) -> ( E. j e. _om p = ( i e.g j ) -> E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
39	38	reximdv	\|- ( ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) -> ( E. i e. _om E. j e. _om p = ( i e.g j ) -> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
40	39	com12	\|- ( E. i e. _om E. j e. _om p = ( i e.g j ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) -> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
41	11 40	simplbiim	\|- ( p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } -> ( ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) -> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) ) )
42	41	rexlimiv	\|- ( E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) -> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) )
43		oveq1	\|- ( i = m -> ( i e.g j ) = ( m e.g j ) )
44	43	oveq1d	\|- ( i = m -> ( ( i e.g j ) \|g ( k e.g l ) ) = ( ( m e.g j ) \|g ( k e.g l ) ) )
45	44	eqeq2d	\|- ( i = m -> ( x = ( ( i e.g j ) \|g ( k e.g l ) ) <-> x = ( ( m e.g j ) \|g ( k e.g l ) ) ) )
46	45	rexbidv	\|- ( i = m -> ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) <-> E. l e. _om x = ( ( m e.g j ) \|g ( k e.g l ) ) ) )
47		eqidd	\|- ( i = m -> k = k )
48	47 43	goaleq12d	\|- ( i = m -> A.g k ( i e.g j ) = A.g k ( m e.g j ) )
49	48	eqeq2d	\|- ( i = m -> ( x = A.g k ( i e.g j ) <-> x = A.g k ( m e.g j ) ) )
50	46 49	orbi12d	\|- ( i = m -> ( ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) <-> ( E. l e. _om x = ( ( m e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g j ) ) ) )
51	50	rexbidv	\|- ( i = m -> ( E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) <-> E. k e. _om ( E. l e. _om x = ( ( m e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g j ) ) ) )
52		oveq2	\|- ( j = n -> ( m e.g j ) = ( m e.g n ) )
53	52	oveq1d	\|- ( j = n -> ( ( m e.g j ) \|g ( k e.g l ) ) = ( ( m e.g n ) \|g ( k e.g l ) ) )
54	53	eqeq2d	\|- ( j = n -> ( x = ( ( m e.g j ) \|g ( k e.g l ) ) <-> x = ( ( m e.g n ) \|g ( k e.g l ) ) ) )
55	54	rexbidv	\|- ( j = n -> ( E. l e. _om x = ( ( m e.g j ) \|g ( k e.g l ) ) <-> E. l e. _om x = ( ( m e.g n ) \|g ( k e.g l ) ) ) )
56		eqidd	\|- ( j = n -> k = k )
57	56 52	goaleq12d	\|- ( j = n -> A.g k ( m e.g j ) = A.g k ( m e.g n ) )
58	57	eqeq2d	\|- ( j = n -> ( x = A.g k ( m e.g j ) <-> x = A.g k ( m e.g n ) ) )
59	55 58	orbi12d	\|- ( j = n -> ( ( E. l e. _om x = ( ( m e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g j ) ) <-> ( E. l e. _om x = ( ( m e.g n ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) ) )
60	59	rexbidv	\|- ( j = n -> ( E. k e. _om ( E. l e. _om x = ( ( m e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g j ) ) <-> E. k e. _om ( E. l e. _om x = ( ( m e.g n ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) ) )
61	51 60	cbvrex2vw	\|- ( E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) <-> E. m e. _om E. n e. _om E. k e. _om ( E. l e. _om x = ( ( m e.g n ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) )
62		oveq1	\|- ( k = o -> ( k e.g l ) = ( o e.g l ) )
63	62	oveq2d	\|- ( k = o -> ( ( m e.g n ) \|g ( k e.g l ) ) = ( ( m e.g n ) \|g ( o e.g l ) ) )
64	63	eqeq2d	\|- ( k = o -> ( x = ( ( m e.g n ) \|g ( k e.g l ) ) <-> x = ( ( m e.g n ) \|g ( o e.g l ) ) ) )
65	64	rexbidv	\|- ( k = o -> ( E. l e. _om x = ( ( m e.g n ) \|g ( k e.g l ) ) <-> E. l e. _om x = ( ( m e.g n ) \|g ( o e.g l ) ) ) )
66		id	\|- ( k = o -> k = o )
67		eqidd	\|- ( k = o -> ( m e.g n ) = ( m e.g n ) )
68	66 67	goaleq12d	\|- ( k = o -> A.g k ( m e.g n ) = A.g o ( m e.g n ) )
69	68	eqeq2d	\|- ( k = o -> ( x = A.g k ( m e.g n ) <-> x = A.g o ( m e.g n ) ) )
70	65 69	orbi12d	\|- ( k = o -> ( ( E. l e. _om x = ( ( m e.g n ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) <-> ( E. l e. _om x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) )
71	70	cbvrexvw	\|- ( E. k e. _om ( E. l e. _om x = ( ( m e.g n ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) <-> E. o e. _om ( E. l e. _om x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) )
72	3	ne0ii	\|- _om =/= (/)
73		r19.44zv	\|- ( _om =/= (/) -> ( E. l e. _om ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) <-> ( E. l e. _om x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) )
74	72 73	ax-mp	\|- ( E. l e. _om ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) <-> ( E. l e. _om x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) )
75		eqeq1	\|- ( y = ( m e.g n ) -> ( y = ( i e.g j ) <-> ( m e.g n ) = ( i e.g j ) ) )
76	75	2rexbidv	\|- ( y = ( m e.g n ) -> ( E. i e. _om E. j e. _om y = ( i e.g j ) <-> E. i e. _om E. j e. _om ( m e.g n ) = ( i e.g j ) ) )
77		ovexd	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> ( m e.g n ) e. _V )
78		simpl	\|- ( ( m e. _om /\ n e. _om ) -> m e. _om )
79	43	eqeq2d	\|- ( i = m -> ( ( m e.g n ) = ( i e.g j ) <-> ( m e.g n ) = ( m e.g j ) ) )
80	79	rexbidv	\|- ( i = m -> ( E. j e. _om ( m e.g n ) = ( i e.g j ) <-> E. j e. _om ( m e.g n ) = ( m e.g j ) ) )
81	80	adantl	\|- ( ( ( m e. _om /\ n e. _om ) /\ i = m ) -> ( E. j e. _om ( m e.g n ) = ( i e.g j ) <-> E. j e. _om ( m e.g n ) = ( m e.g j ) ) )
82		simpr	\|- ( ( m e. _om /\ n e. _om ) -> n e. _om )
83	52	eqeq2d	\|- ( j = n -> ( ( m e.g n ) = ( m e.g j ) <-> ( m e.g n ) = ( m e.g n ) ) )
84	83	adantl	\|- ( ( ( m e. _om /\ n e. _om ) /\ j = n ) -> ( ( m e.g n ) = ( m e.g j ) <-> ( m e.g n ) = ( m e.g n ) ) )
85		eqidd	\|- ( ( m e. _om /\ n e. _om ) -> ( m e.g n ) = ( m e.g n ) )
86	82 84 85	rspcedvd	\|- ( ( m e. _om /\ n e. _om ) -> E. j e. _om ( m e.g n ) = ( m e.g j ) )
87	78 81 86	rspcedvd	\|- ( ( m e. _om /\ n e. _om ) -> E. i e. _om E. j e. _om ( m e.g n ) = ( i e.g j ) )
88	87	ad3antrrr	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> E. i e. _om E. j e. _om ( m e.g n ) = ( i e.g j ) )
89	76 77 88	elrabd	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> ( m e.g n ) e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } )
90		oveq1	\|- ( p = ( m e.g n ) -> ( p \|g q ) = ( ( m e.g n ) \|g q ) )
91	90	eqeq2d	\|- ( p = ( m e.g n ) -> ( x = ( p \|g q ) <-> x = ( ( m e.g n ) \|g q ) ) )
92	91	rexbidv	\|- ( p = ( m e.g n ) -> ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) <-> E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) \|g q ) ) )
93		eqidd	\|- ( p = ( m e.g n ) -> k = k )
94		id	\|- ( p = ( m e.g n ) -> p = ( m e.g n ) )
95	93 94	goaleq12d	\|- ( p = ( m e.g n ) -> A.g k p = A.g k ( m e.g n ) )
96	95	eqeq2d	\|- ( p = ( m e.g n ) -> ( x = A.g k p <-> x = A.g k ( m e.g n ) ) )
97	96	rexbidv	\|- ( p = ( m e.g n ) -> ( E. k e. _om x = A.g k p <-> E. k e. _om x = A.g k ( m e.g n ) ) )
98	92 97	orbi12d	\|- ( p = ( m e.g n ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) <-> ( E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) \|g q ) \/ E. k e. _om x = A.g k ( m e.g n ) ) ) )
99	98	adantl	\|- ( ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) /\ p = ( m e.g n ) ) -> ( ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) <-> ( E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) \|g q ) \/ E. k e. _om x = A.g k ( m e.g n ) ) ) )
100		ovexd	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( o e.g l ) e. _V )
101		simpr	\|- ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) -> o e. _om )
102	101	adantr	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> o e. _om )
103		oveq1	\|- ( i = o -> ( i e.g j ) = ( o e.g j ) )
104	103	eqeq2d	\|- ( i = o -> ( ( o e.g l ) = ( i e.g j ) <-> ( o e.g l ) = ( o e.g j ) ) )
105	104	rexbidv	\|- ( i = o -> ( E. j e. _om ( o e.g l ) = ( i e.g j ) <-> E. j e. _om ( o e.g l ) = ( o e.g j ) ) )
106	105	adantl	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ i = o ) -> ( E. j e. _om ( o e.g l ) = ( i e.g j ) <-> E. j e. _om ( o e.g l ) = ( o e.g j ) ) )
107		simpr	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> l e. _om )
108		oveq2	\|- ( j = l -> ( o e.g j ) = ( o e.g l ) )
109	108	eqeq2d	\|- ( j = l -> ( ( o e.g l ) = ( o e.g j ) <-> ( o e.g l ) = ( o e.g l ) ) )
110	109	adantl	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ j = l ) -> ( ( o e.g l ) = ( o e.g j ) <-> ( o e.g l ) = ( o e.g l ) ) )
111		eqidd	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( o e.g l ) = ( o e.g l ) )
112	107 110 111	rspcedvd	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> E. j e. _om ( o e.g l ) = ( o e.g j ) )
113	102 106 112	rspcedvd	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> E. i e. _om E. j e. _om ( o e.g l ) = ( i e.g j ) )
114		eqeq1	\|- ( p = ( o e.g l ) -> ( p = ( i e.g j ) <-> ( o e.g l ) = ( i e.g j ) ) )
115	114	2rexbidv	\|- ( p = ( o e.g l ) -> ( E. i e. _om E. j e. _om p = ( i e.g j ) <-> E. i e. _om E. j e. _om ( o e.g l ) = ( i e.g j ) ) )
116		fmla0	\|- ( Fmla ` (/) ) = { p e. _V \| E. i e. _om E. j e. _om p = ( i e.g j ) }
117	115 116	elrab2	\|- ( ( o e.g l ) e. ( Fmla ` (/) ) <-> ( ( o e.g l ) e. _V /\ E. i e. _om E. j e. _om ( o e.g l ) = ( i e.g j ) ) )
118	100 113 117	sylanbrc	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( o e.g l ) e. ( Fmla ` (/) ) )
119	118	adantr	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = ( ( m e.g n ) \|g ( o e.g l ) ) ) -> ( o e.g l ) e. ( Fmla ` (/) ) )
120		oveq2	\|- ( q = ( o e.g l ) -> ( ( m e.g n ) \|g q ) = ( ( m e.g n ) \|g ( o e.g l ) ) )
121	120	eqeq2d	\|- ( q = ( o e.g l ) -> ( x = ( ( m e.g n ) \|g q ) <-> x = ( ( m e.g n ) \|g ( o e.g l ) ) ) )
122	121	adantl	\|- ( ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = ( ( m e.g n ) \|g ( o e.g l ) ) ) /\ q = ( o e.g l ) ) -> ( x = ( ( m e.g n ) \|g q ) <-> x = ( ( m e.g n ) \|g ( o e.g l ) ) ) )
123		simpr	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = ( ( m e.g n ) \|g ( o e.g l ) ) ) -> x = ( ( m e.g n ) \|g ( o e.g l ) ) )
124	119 122 123	rspcedvd	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = ( ( m e.g n ) \|g ( o e.g l ) ) ) -> E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) \|g q ) )
125	124	ex	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( x = ( ( m e.g n ) \|g ( o e.g l ) ) -> E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) \|g q ) ) )
126	102	adantr	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = A.g o ( m e.g n ) ) -> o e. _om )
127	69	adantl	\|- ( ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = A.g o ( m e.g n ) ) /\ k = o ) -> ( x = A.g k ( m e.g n ) <-> x = A.g o ( m e.g n ) ) )
128		simpr	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = A.g o ( m e.g n ) ) -> x = A.g o ( m e.g n ) )
129	126 127 128	rspcedvd	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ x = A.g o ( m e.g n ) ) -> E. k e. _om x = A.g k ( m e.g n ) )
130	129	ex	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( x = A.g o ( m e.g n ) -> E. k e. _om x = A.g k ( m e.g n ) ) )
131	125 130	orim12d	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> ( E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) \|g q ) \/ E. k e. _om x = A.g k ( m e.g n ) ) ) )
132	131	imp	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> ( E. q e. ( Fmla ` (/) ) x = ( ( m e.g n ) \|g q ) \/ E. k e. _om x = A.g k ( m e.g n ) ) )
133	89 99 132	rspcedvd	\|- ( ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) /\ ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) ) -> E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) )
134	133	ex	\|- ( ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) /\ l e. _om ) -> ( ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) ) )
135	134	rexlimdva	\|- ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) -> ( E. l e. _om ( x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) ) )
136	74 135	biimtrrid	\|- ( ( ( m e. _om /\ n e. _om ) /\ o e. _om ) -> ( ( E. l e. _om x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) ) )
137	136	rexlimdva	\|- ( ( m e. _om /\ n e. _om ) -> ( E. o e. _om ( E. l e. _om x = ( ( m e.g n ) \|g ( o e.g l ) ) \/ x = A.g o ( m e.g n ) ) -> E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) ) )
138	71 137	biimtrid	\|- ( ( m e. _om /\ n e. _om ) -> ( E. k e. _om ( E. l e. _om x = ( ( m e.g n ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) -> E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) ) )
139	138	rexlimivv	\|- ( E. m e. _om E. n e. _om E. k e. _om ( E. l e. _om x = ( ( m e.g n ) \|g ( k e.g l ) ) \/ x = A.g k ( m e.g n ) ) -> E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) )
140	61 139	sylbi	\|- ( E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) -> E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) )
141	42 140	impbii	\|- ( E. p e. { y e. _V \| E. i e. _om E. j e. _om y = ( i e.g j ) } ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) <-> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) )
142	8 141	bitri	\|- ( E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) <-> E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) )
143	142	abbii	\|- { x \| E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) } = { x \| E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) }
144	6 143	uneq12i	\|- ( ( Fmla ` (/) ) u. { x \| E. p e. ( Fmla ` (/) ) ( E. q e. ( Fmla ` (/) ) x = ( p \|g q ) \/ E. k e. _om x = A.g k p ) } ) = ( ( { (/) } X. ( _om X. _om ) ) u. { x \| E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) } )
145	2 5 144	3eqtri	\|- ( Fmla ` 1o ) = ( ( { (/) } X. ( _om X. _om ) ) u. { x \| E. i e. _om E. j e. _om E. k e. _om ( E. l e. _om x = ( ( i e.g j ) \|g ( k e.g l ) ) \/ x = A.g k ( i e.g j ) ) } )

Metamath Proof Explorer

Theorem fmla1

Proof