fmla1 - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fmla1		Structured version Visualization version GIF version

Theorem fmla1 34367

Description: The valid Godel formulas of height 1 is the set of all formulas of the form (𝑎⊼_𝑔𝑏) and ∀_𝑔𝑘𝑎 with atoms 𝑎, 𝑏 of the form 𝑥 ∈ 𝑦. (Contributed by AV, 20-Sep-2023.)

**Assertion**
Ref	Expression
fmla1	⊢ (Fmla‘1_o) = (({∅} × (ω × ω)) ∪ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))})

Distinct variable group: 𝑖,𝑗,𝑥,𝑘,𝑙

Proof of Theorem fmla1 Dummy variables 𝑦 𝑛 𝑧 𝑚 𝑜 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-1o 8463	. . 3 ⊢ 1_o = suc ∅
2	1	fveq2i 6892	. 2 ⊢ (Fmla‘1_o) = (Fmla‘suc ∅)
3		peano1 7876	. . 3 ⊢ ∅ ∈ ω
4		fmlasuc 34366	. . 3 ⊢ (∅ ∈ ω → (Fmla‘suc ∅) = ((Fmla‘∅) ∪ {𝑥 ∣ ∃𝑝 ∈ (Fmla‘∅)(∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝)}))
5	3, 4	ax-mp 5	. 2 ⊢ (Fmla‘suc ∅) = ((Fmla‘∅) ∪ {𝑥 ∣ ∃𝑝 ∈ (Fmla‘∅)(∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝)})
6		fmla0xp 34363	. . 3 ⊢ (Fmla‘∅) = ({∅} × (ω × ω))
7		fmla0 34362	. . . . . 6 ⊢ (Fmla‘∅) = {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)}
8	7	rexeqi 3325	. . . . 5 ⊢ (∃𝑝 ∈ (Fmla‘∅)(∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) ↔ ∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝))
9		eqeq1 2737	. . . . . . . . . 10 ⊢ (𝑦 = 𝑝 → (𝑦 = (𝑖∈_𝑔𝑗) ↔ 𝑝 = (𝑖∈_𝑔𝑗)))
10	9	2rexbidv 3220	. . . . . . . . 9 ⊢ (𝑦 = 𝑝 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑝 = (𝑖∈_𝑔𝑗)))
11	10	elrab 3683	. . . . . . . 8 ⊢ (𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} ↔ (𝑝 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑝 = (𝑖∈_𝑔𝑗)))
12		oveq1 7413	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → (𝑝⊼_𝑔𝑞) = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞))
13	12	eqeq2d 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → (𝑥 = (𝑝⊼_𝑔𝑞) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞)))
14	13	rexbidv 3179	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ↔ ∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞)))
15		eqidd 2734	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → 𝑘 = 𝑘)
16		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → 𝑝 = (𝑖∈_𝑔𝑗))
17	15, 16	goaleq12d 34331	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → ∀_𝑔𝑘𝑝 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))
18	17	eqeq2d 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → (𝑥 = ∀_𝑔𝑘𝑝 ↔ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)))
19	18	rexbidv 3179	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → (∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝 ↔ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)))
20	14, 19	orbi12d 918	. . . . . . . . . . . . 13 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → ((∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) ↔ (∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))))
21		eqeq1 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑞 → (𝑧 = (𝑘∈_𝑔𝑙) ↔ 𝑞 = (𝑘∈_𝑔𝑙)))
22	21	2rexbidv 3220	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑞 → (∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑧 = (𝑘∈_𝑔𝑙) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑞 = (𝑘∈_𝑔𝑙)))
23		fmla0 34362	. . . . . . . . . . . . . . . . . 18 ⊢ (Fmla‘∅) = {𝑧 ∈ V ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑧 = (𝑘∈_𝑔𝑙)}
24	22, 23	elrab2 3686	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ (Fmla‘∅) ↔ (𝑞 ∈ V ∧ ∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑞 = (𝑘∈_𝑔𝑙)))
25		oveq2 7414	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = (𝑘∈_𝑔𝑙) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
26	25	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑞 = (𝑘∈_𝑔𝑙) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
27	26	biimpcd 248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) → (𝑞 = (𝑘∈_𝑔𝑙) → 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
28	27	reximdv 3171	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) → (∃𝑙 ∈ ω 𝑞 = (𝑘∈_𝑔𝑙) → ∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
29	28	reximdv 3171	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑞 = (𝑘∈_𝑔𝑙) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
30	29	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑞 = (𝑘∈_𝑔𝑙) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
31	24, 30	simplbiim 506	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ (Fmla‘∅) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
32	31	rexlimiv 3149	. . . . . . . . . . . . . . 15 ⊢ (∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
33	32	orim1i 909	. . . . . . . . . . . . . 14 ⊢ ((∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)))
34		r19.43 3123	. . . . . . . . . . . . . 14 ⊢ (∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)))
35	33, 34	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)) → ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)))
36	20, 35	syl6bi 253	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑖∈_𝑔𝑗) → ((∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) → ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))))
37	36	com12 32	. . . . . . . . . . 11 ⊢ ((∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) → (𝑝 = (𝑖∈_𝑔𝑗) → ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))))
38	37	reximdv 3171	. . . . . . . . . 10 ⊢ ((∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) → (∃𝑗 ∈ ω 𝑝 = (𝑖∈_𝑔𝑗) → ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))))
39	38	reximdv 3171	. . . . . . . . 9 ⊢ ((∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑝 = (𝑖∈_𝑔𝑗) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))))
40	39	com12 32	. . . . . . . 8 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑝 = (𝑖∈_𝑔𝑗) → ((∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))))
41	11, 40	simplbiim 506	. . . . . . 7 ⊢ (𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} → ((∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))))
42	41	rexlimiv 3149	. . . . . 6 ⊢ (∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)))
43		oveq1 7413	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑚 → (𝑖∈_𝑔𝑗) = (𝑚∈_𝑔𝑗))
44	43	oveq1d 7421	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑚 → ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) = ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
45	44	eqeq2d 2744	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑚 → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ↔ 𝑥 = ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
46	45	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝑖 = 𝑚 → (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ↔ ∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
47		eqidd 2734	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑚 → 𝑘 = 𝑘)
48	47, 43	goaleq12d 34331	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑚 → ∀_𝑔𝑘(𝑖∈_𝑔𝑗) = ∀_𝑔𝑘(𝑚∈_𝑔𝑗))
49	48	eqeq2d 2744	. . . . . . . . . 10 ⊢ (𝑖 = 𝑚 → (𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗) ↔ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑗)))
50	46, 49	orbi12d 918	. . . . . . . . 9 ⊢ (𝑖 = 𝑚 → ((∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)) ↔ (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑗))))
51	50	rexbidv 3179	. . . . . . . 8 ⊢ (𝑖 = 𝑚 → (∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)) ↔ ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑗))))
52		oveq2 7414	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑛 → (𝑚∈_𝑔𝑗) = (𝑚∈_𝑔𝑛))
53	52	oveq1d 7421	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑛 → ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)))
54	53	eqeq2d 2744	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → (𝑥 = ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ↔ 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙))))
55	54	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝑗 = 𝑛 → (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ↔ ∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙))))
56		eqidd 2734	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑛 → 𝑘 = 𝑘)
57	56, 52	goaleq12d 34331	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → ∀_𝑔𝑘(𝑚∈_𝑔𝑗) = ∀_𝑔𝑘(𝑚∈_𝑔𝑛))
58	57	eqeq2d 2744	. . . . . . . . . 10 ⊢ (𝑗 = 𝑛 → (𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑗) ↔ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)))
59	55, 58	orbi12d 918	. . . . . . . . 9 ⊢ (𝑗 = 𝑛 → ((∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑗)) ↔ (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛))))
60	59	rexbidv 3179	. . . . . . . 8 ⊢ (𝑗 = 𝑛 → (∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑗)) ↔ ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛))))
61	51, 60	cbvrex2vw 3240	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)) ↔ ∃𝑚 ∈ ω ∃𝑛 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)))
62		oveq1 7413	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑜 → (𝑘∈_𝑔𝑙) = (𝑜∈_𝑔𝑙))
63	62	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑜 → ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)))
64	63	eqeq2d 2744	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑜 → (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) ↔ 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙))))
65	64	rexbidv 3179	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑜 → (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) ↔ ∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙))))
66		id 22	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑜 → 𝑘 = 𝑜)
67		eqidd 2734	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑜 → (𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑛))
68	66, 67	goaleq12d 34331	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑜 → ∀_𝑔𝑘(𝑚∈_𝑔𝑛) = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))
69	68	eqeq2d 2744	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑜 → (𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛) ↔ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)))
70	65, 69	orbi12d 918	. . . . . . . . . 10 ⊢ (𝑘 = 𝑜 → ((∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)) ↔ (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))))
71	70	cbvrexvw 3236	. . . . . . . . 9 ⊢ (∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)) ↔ ∃𝑜 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)))
72	3	ne0ii 4337	. . . . . . . . . . . 12 ⊢ ω ≠ ∅
73		r19.44zv 4503	. . . . . . . . . . . 12 ⊢ (ω ≠ ∅ → (∃𝑙 ∈ ω (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) ↔ (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))))
74	72, 73	ax-mp 5	. . . . . . . . . . 11 ⊢ (∃𝑙 ∈ ω (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) ↔ (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)))
75		eqeq1 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑚∈_𝑔𝑛) → (𝑦 = (𝑖∈_𝑔𝑗) ↔ (𝑚∈_𝑔𝑛) = (𝑖∈_𝑔𝑗)))
76	75	2rexbidv 3220	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑚∈_𝑔𝑛) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑚∈_𝑔𝑛) = (𝑖∈_𝑔𝑗)))
77		ovexd 7441	. . . . . . . . . . . . . . 15 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))) → (𝑚∈_𝑔𝑛) ∈ V)
78		simpl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → 𝑚 ∈ ω)
79	43	eqeq2d 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑚 → ((𝑚∈_𝑔𝑛) = (𝑖∈_𝑔𝑗) ↔ (𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑗)))
80	79	rexbidv 3179	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑚 → (∃𝑗 ∈ ω (𝑚∈_𝑔𝑛) = (𝑖∈_𝑔𝑗) ↔ ∃𝑗 ∈ ω (𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑗)))
81	80	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑖 = 𝑚) → (∃𝑗 ∈ ω (𝑚∈_𝑔𝑛) = (𝑖∈_𝑔𝑗) ↔ ∃𝑗 ∈ ω (𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑗)))
82		simpr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
83	52	eqeq2d 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑛 → ((𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑗) ↔ (𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑛)))
84	83	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑗 = 𝑛) → ((𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑗) ↔ (𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑛)))
85		eqidd 2734	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑛))
86	82, 84, 85	rspcedvd 3615	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → ∃𝑗 ∈ ω (𝑚∈_𝑔𝑛) = (𝑚∈_𝑔𝑗))
87	78, 81, 86	rspcedvd 3615	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑚∈_𝑔𝑛) = (𝑖∈_𝑔𝑗))
88	87	ad5ant12 755	. . . . . . . . . . . . . . 15 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑚∈_𝑔𝑛) = (𝑖∈_𝑔𝑗))
89	76, 77, 88	elrabd 3685	. . . . . . . . . . . . . 14 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))) → (𝑚∈_𝑔𝑛) ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)})
90		oveq1 7413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (𝑚∈_𝑔𝑛) → (𝑝⊼_𝑔𝑞) = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞))
91	90	eqeq2d 2744	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (𝑚∈_𝑔𝑛) → (𝑥 = (𝑝⊼_𝑔𝑞) ↔ 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞)))
92	91	rexbidv 3179	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑚∈_𝑔𝑛) → (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ↔ ∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞)))
93		eqidd 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = (𝑚∈_𝑔𝑛) → 𝑘 = 𝑘)
94		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = (𝑚∈_𝑔𝑛) → 𝑝 = (𝑚∈_𝑔𝑛))
95	93, 94	goaleq12d 34331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (𝑚∈_𝑔𝑛) → ∀_𝑔𝑘𝑝 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛))
96	95	eqeq2d 2744	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (𝑚∈_𝑔𝑛) → (𝑥 = ∀_𝑔𝑘𝑝 ↔ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)))
97	96	rexbidv 3179	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑚∈_𝑔𝑛) → (∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝 ↔ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)))
98	92, 97	orbi12d 918	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (𝑚∈_𝑔𝑛) → ((∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) ↔ (∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛))))
99	98	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))) ∧ 𝑝 = (𝑚∈_𝑔𝑛)) → ((∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) ↔ (∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛))))
100		ovexd 7441	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → (𝑜∈_𝑔𝑙) ∈ V)
101		simpr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) → 𝑜 ∈ ω)
102	101	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → 𝑜 ∈ ω)
103		oveq1 7413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑜 → (𝑖∈_𝑔𝑗) = (𝑜∈_𝑔𝑗))
104	103	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑜 → ((𝑜∈_𝑔𝑙) = (𝑖∈_𝑔𝑗) ↔ (𝑜∈_𝑔𝑙) = (𝑜∈_𝑔𝑗)))
105	104	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑜 → (∃𝑗 ∈ ω (𝑜∈_𝑔𝑙) = (𝑖∈_𝑔𝑗) ↔ ∃𝑗 ∈ ω (𝑜∈_𝑔𝑙) = (𝑜∈_𝑔𝑗)))
106	105	adantl 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑖 = 𝑜) → (∃𝑗 ∈ ω (𝑜∈_𝑔𝑙) = (𝑖∈_𝑔𝑗) ↔ ∃𝑗 ∈ ω (𝑜∈_𝑔𝑙) = (𝑜∈_𝑔𝑗)))
107		simpr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → 𝑙 ∈ ω)
108		oveq2 7414	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 𝑙 → (𝑜∈_𝑔𝑗) = (𝑜∈_𝑔𝑙))
109	108	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 𝑙 → ((𝑜∈_𝑔𝑙) = (𝑜∈_𝑔𝑗) ↔ (𝑜∈_𝑔𝑙) = (𝑜∈_𝑔𝑙)))
110	109	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑗 = 𝑙) → ((𝑜∈_𝑔𝑙) = (𝑜∈_𝑔𝑗) ↔ (𝑜∈_𝑔𝑙) = (𝑜∈_𝑔𝑙)))
111		eqidd 2734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → (𝑜∈_𝑔𝑙) = (𝑜∈_𝑔𝑙))
112	107, 110, 111	rspcedvd 3615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → ∃𝑗 ∈ ω (𝑜∈_𝑔𝑙) = (𝑜∈_𝑔𝑗))
113	102, 106, 112	rspcedvd 3615	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑜∈_𝑔𝑙) = (𝑖∈_𝑔𝑗))
114		eqeq1 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = (𝑜∈_𝑔𝑙) → (𝑝 = (𝑖∈_𝑔𝑗) ↔ (𝑜∈_𝑔𝑙) = (𝑖∈_𝑔𝑗)))
115	114	2rexbidv 3220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = (𝑜∈_𝑔𝑙) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑝 = (𝑖∈_𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑜∈_𝑔𝑙) = (𝑖∈_𝑔𝑗)))
116		fmla0 34362	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fmla‘∅) = {𝑝 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑝 = (𝑖∈_𝑔𝑗)}
117	115, 116	elrab2 3686	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑜∈_𝑔𝑙) ∈ (Fmla‘∅) ↔ ((𝑜∈_𝑔𝑙) ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑜∈_𝑔𝑙) = (𝑖∈_𝑔𝑗)))
118	100, 113, 117	sylanbrc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → (𝑜∈_𝑔𝑙) ∈ (Fmla‘∅))
119	118	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙))) → (𝑜∈_𝑔𝑙) ∈ (Fmla‘∅))
120		oveq2 7414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 = (𝑜∈_𝑔𝑙) → ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞) = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)))
121	120	eqeq2d 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = (𝑜∈_𝑔𝑙) → (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞) ↔ 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙))))
122	121	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙))) ∧ 𝑞 = (𝑜∈_𝑔𝑙)) → (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞) ↔ 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙))))
123		simpr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙))) → 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)))
124	119, 122, 123	rspcedvd 3615	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙))) → ∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞))
125	124	ex 414	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) → ∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞)))
126	102	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) → 𝑜 ∈ ω)
127	69	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) ∧ 𝑘 = 𝑜) → (𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛) ↔ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)))
128		simpr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) → 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))
129	126, 127, 128	rspcedvd 3615	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) → ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛))
130	129	ex 414	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → (𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛) → ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)))
131	125, 130	orim12d 964	. . . . . . . . . . . . . . 15 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → ((𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) → (∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛))))
132	131	imp 408	. . . . . . . . . . . . . 14 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))) → (∃𝑞 ∈ (Fmla‘∅)𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)))
133	89, 99, 132	rspcedvd 3615	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) ∧ (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛))) → ∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝))
134	133	ex 414	. . . . . . . . . . . 12 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) ∧ 𝑙 ∈ ω) → ((𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) → ∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝)))
135	134	rexlimdva 3156	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) → (∃𝑙 ∈ ω (𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) → ∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝)))
136	74, 135	biimtrrid 242	. . . . . . . . . 10 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑜 ∈ ω) → ((∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) → ∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝)))
137	136	rexlimdva 3156	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (∃𝑜 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑜∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑜(𝑚∈_𝑔𝑛)) → ∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝)))
138	71, 137	biimtrid 241	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)) → ∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝)))
139	138	rexlimivv 3200	. . . . . . 7 ⊢ (∃𝑚 ∈ ω ∃𝑛 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑚∈_𝑔𝑛)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑚∈_𝑔𝑛)) → ∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝))
140	61, 139	sylbi 216	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)) → ∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝))
141	42, 140	impbii 208	. . . . 5 ⊢ (∃𝑝 ∈ {𝑦 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈_𝑔𝑗)} (∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)))
142	8, 141	bitri 275	. . . 4 ⊢ (∃𝑝 ∈ (Fmla‘∅)(∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗)))
143	142	abbii 2803	. . 3 ⊢ {𝑥 ∣ ∃𝑝 ∈ (Fmla‘∅)(∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝)} = {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))}
144	6, 143	uneq12i 4161	. 2 ⊢ ((Fmla‘∅) ∪ {𝑥 ∣ ∃𝑝 ∈ (Fmla‘∅)(∃𝑞 ∈ (Fmla‘∅)𝑥 = (𝑝⊼_𝑔𝑞) ∨ ∃𝑘 ∈ ω 𝑥 = ∀_𝑔𝑘𝑝)}) = (({∅} × (ω × ω)) ∪ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))})
145	2, 5, 144	3eqtri 2765	1 ⊢ (Fmla‘1_o) = (({∅} × (ω × ω)) ∪ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∨ 𝑥 = ∀_𝑔𝑘(𝑖∈_𝑔𝑗))})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 {cab 2710 ≠ wne 2941 ∃wrex 3071 {crab 3433 Vcvv 3475 ∪ cun 3946 ∅c0 4322 {csn 4628 × cxp 5674 suc csuc 6364 ‘cfv 6541 (class class class)co 7406 ωcom 7852 1_oc1o 8456 ∈_𝑔cgoe 34313 ⊼_𝑔cgna 34314 ∀_𝑔cgol 34315 Fmlacfmla 34317

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-ov 7409 df-oprab 7410 df-mpo 7411 df-om 7853 df-1st 7972 df-2nd 7973 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-map 8819 df-goel 34320 df-goal 34322 df-sat 34323 df-fmla 34325

This theorem is referenced by: 2goelgoanfmla1 34404

W3C validator