Theorem ralcom2 1774

Description: Commutation of restricted quantifiers. Note that x and y needn't be distinct (this makes the proof longer but illustrates the use of dvelim 1351).

Assertion

Ref	Expression
ralcom2	⊢ (∀x ∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ)

Distinct variable groups:   y,A   x,A

Proof of Theorem ralcom2

Step	Hyp	Ref	Expression
1		id 59	. . . 4 ⊢ (∀x(x ∈ A → ∀x(x ∈ A → φ)) → ∀x(x ∈ A → ∀x(x ∈ A → φ)))
2		eleq1 1532	. . . . . . . . . 10 ⊢ (x = y → (x ∈ A ↔ y ∈ A))
3	2	a4s 983	. . . . . . . . 9 ⊢ (∀x x = y → (x ∈ A ↔ y ∈ A))
4	3	imbi1d 612	. . . . . . . 8 ⊢ (∀x x = y → ((x ∈ A → φ) ↔ (y ∈ A → φ)))
5	4	dral1 1153	. . . . . . 7 ⊢ (∀x x = y → (∀x(x ∈ A → φ) ↔ ∀y(y ∈ A → φ)))
6	5	imbi2d 611	. . . . . 6 ⊢ (∀x x = y → ((x ∈ A → ∀x(x ∈ A → φ)) ↔ (x ∈ A → ∀y(y ∈ A → φ))))
7	6	dral2 1154	. . . . 5 ⊢ (∀x x = y → (∀x(x ∈ A → ∀x(x ∈ A → φ)) ↔ ∀x(x ∈ A → ∀y(y ∈ A → φ))))
8	3	imbi1d 612	. . . . . 6 ⊢ (∀x x = y → ((x ∈ A → ∀x(x ∈ A → φ)) ↔ (y ∈ A → ∀x(x ∈ A → φ))))
9	8	dral1 1153	. . . . 5 ⊢ (∀x x = y → (∀x(x ∈ A → ∀x(x ∈ A → φ)) ↔ ∀y(y ∈ A → ∀x(x ∈ A → φ))))
10	7, 9	imbi12d 625	. . . 4 ⊢ (∀x x = y → ((∀x(x ∈ A → ∀x(x ∈ A → φ)) → ∀x(x ∈ A → ∀x(x ∈ A → φ))) ↔ (∀x(x ∈ A → ∀y(y ∈ A → φ)) → ∀y(y ∈ A → ∀x(x ∈ A → φ)))))
11	1, 10	mpbii 193	. . 3 ⊢ (∀x x = y → (∀x(x ∈ A → ∀y(y ∈ A → φ)) → ∀y(y ∈ A → ∀x(x ∈ A → φ))))
12		hbnae 1146	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
13	12	hbal 1004	. . . . . 6 ⊢ (∀y ¬ ∀x x = y → ∀x∀y ¬ ∀x x = y)
14		hbnae 1146	. . . . . . . 8 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
15		ax-17 970	. . . . . . . . . 10 ⊢ (z ∈ A → ∀y z ∈ A)
16		eleq1 1532	. . . . . . . . . 10 ⊢ (z = x → (z ∈ A ↔ x ∈ A))
17	15, 16	dvelim 1351	. . . . . . . . 9 ⊢ (¬ ∀y y = x → (x ∈ A → ∀y x ∈ A))
18	17	nalequcoms 1143	. . . . . . . 8 ⊢ (¬ ∀x x = y → (x ∈ A → ∀y x ∈ A))
19		hba1 1002	. . . . . . . . 9 ⊢ (∀y(y ∈ A → φ) → ∀y∀y(y ∈ A → φ))
20	19	a1i 8	. . . . . . . 8 ⊢ (¬ ∀x x = y → (∀y(y ∈ A → φ) → ∀y∀y(y ∈ A → φ)))
21	14, 18, 20	hbimd 1109	. . . . . . 7 ⊢ (¬ ∀x x = y → ((x ∈ A → ∀y(y ∈ A → φ)) → ∀y(x ∈ A → ∀y(y ∈ A → φ))))
22	21	a4s 983	. . . . . 6 ⊢ (∀y ¬ ∀x x = y → ((x ∈ A → ∀y(y ∈ A → φ)) → ∀y(x ∈ A → ∀y(y ∈ A → φ))))
23	13, 22	hbald 1112	. . . . 5 ⊢ (∀y ¬ ∀x x = y → (∀x(x ∈ A → ∀y(y ∈ A → φ)) → ∀y∀x(x ∈ A → ∀y(y ∈ A → φ))))
24		ax-17 970	. . . . . . . 8 ⊢ (z ∈ A → ∀x z ∈ A)
25		eleq1 1532	. . . . . . . 8 ⊢ (z = y → (z ∈ A ↔ y ∈ A))
26	24, 25	dvelim 1351	. . . . . . 7 ⊢ (¬ ∀x x = y → (y ∈ A → ∀x y ∈ A))
27		ax-4 972	. . . . . . . . . 10 ⊢ (∀y(y ∈ A → φ) → (y ∈ A → φ))
28	27	imim2i 17	. . . . . . . . 9 ⊢ ((x ∈ A → ∀y(y ∈ A → φ)) → (x ∈ A → (y ∈ A → φ)))
29	28	com23 32	. . . . . . . 8 ⊢ ((x ∈ A → ∀y(y ∈ A → φ)) → (y ∈ A → (x ∈ A → φ)))
30	29	19.20ii 994	. . . . . . 7 ⊢ (∀x(x ∈ A → ∀y(y ∈ A → φ)) → (∀x y ∈ A → ∀x(x ∈ A → φ)))
31	26, 30	syl9 57	. . . . . 6 ⊢ (¬ ∀x x = y → (∀x(x ∈ A → ∀y(y ∈ A → φ)) → (y ∈ A → ∀x(x ∈ A → φ))))
32	31	19.20ii 994	. . . . 5 ⊢ (∀y ¬ ∀x x = y → (∀y∀x(x ∈ A → ∀y(y ∈ A → φ)) → ∀y(y ∈ A → ∀x(x ∈ A → φ))))
33	23, 32	syld 27	. . . 4 ⊢ (∀y ¬ ∀x x = y → (∀x(x ∈ A → ∀y(y ∈ A → φ)) → ∀y(y ∈ A → ∀x(x ∈ A → φ))))
34	33	hbnaes 1147	. . 3 ⊢ (¬ ∀x x = y → (∀x(x ∈ A → ∀y(y ∈ A → φ)) → ∀y(y ∈ A → ∀x(x ∈ A → φ))))
35	11, 34	pm2.61i 126	. 2 ⊢ (∀x(x ∈ A → ∀y(y ∈ A → φ)) → ∀y(y ∈ A → ∀x(x ∈ A → φ)))
36		df-ral 1647	. . 3 ⊢ (∀x ∈ A ∀y ∈ A φ ↔ ∀x(x ∈ A → ∀y ∈ A φ))
37		df-ral 1647	. . . . 5 ⊢ (∀y ∈ A φ ↔ ∀y(y ∈ A → φ))
38	37	imbi2i 185	. . . 4 ⊢ ((x ∈ A → ∀y ∈ A φ) ↔ (x ∈ A → ∀y(y ∈ A → φ)))
39	38	albii 998	. . 3 ⊢ (∀x(x ∈ A → ∀y ∈ A φ) ↔ ∀x(x ∈ A → ∀y(y ∈ A → φ)))
40	36, 39	bitr 173	. 2 ⊢ (∀x ∈ A ∀y ∈ A φ ↔ ∀x(x ∈ A → ∀y(y ∈ A → φ)))
41		df-ral 1647	. . 3 ⊢ (∀y ∈ A ∀x ∈ A φ ↔ ∀y(y ∈ A → ∀x ∈ A φ))
42		df-ral 1647	. . . . 5 ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
43	42	imbi2i 185	. . . 4 ⊢ ((y ∈ A → ∀x ∈ A φ) ↔ (y ∈ A → ∀x(x ∈ A → φ)))
44	43	albii 998	. . 3 ⊢ (∀y(y ∈ A → ∀x ∈ A φ) ↔ ∀y(y ∈ A → ∀x(x ∈ A → φ)))
45	41, 44	bitr 173	. 2 ⊢ (∀y ∈ A ∀x ∈ A φ ↔ ∀y(y ∈ A → ∀x(x ∈ A → φ)))
46	35, 40, 45	3imtr4 219	1 ⊢ (∀x ∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ)

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146  ∀wal 953   = wceq 955   ∈ wcel 957  ∀wral 1643

This theorem is referenced by:  tz7.48lem 3950

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-cleq 1468  df-clel 1471  df-ral 1647

Copyright terms: Public domain