Theorem marypha1lem 9038

Description: Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.)

Assertion

Ref	Expression
marypha1lem	⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))

Distinct variable group:   𝐴,𝑏,𝑐,𝑑,𝑒

Proof of Theorem marypha1lem

Dummy variables 𝑎 𝑓 𝑔 ℎ 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpeq1 5554	. . . . 5 ⊢ (𝑎 = 𝑓 → (𝑎 × 𝑏) = (𝑓 × 𝑏))
2	1	pweqd 4522	. . . 4 ⊢ (𝑎 = 𝑓 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝑓 × 𝑏))
3		pweq 4519	. . . . . 6 ⊢ (𝑎 = 𝑓 → 𝒫 𝑎 = 𝒫 𝑓)
4	3	raleqdv 3318	. . . . 5 ⊢ (𝑎 = 𝑓 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
5		f1eq2 6600	. . . . . 6 ⊢ (𝑎 = 𝑓 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝑓–1-1→V))
6	5	rexbidv 3209	. . . . 5 ⊢ (𝑎 = 𝑓 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
7	4, 6	imbi12d 348	. . . 4 ⊢ (𝑎 = 𝑓 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
8	2, 7	raleqbidv 3306	. . 3 ⊢ (𝑎 = 𝑓 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
9	8	imbi2d 344	. 2 ⊢ (𝑎 = 𝑓 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
10		xpeq1 5554	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑏) = (𝐴 × 𝑏))
11	10	pweqd 4522	. . . 4 ⊢ (𝑎 = 𝐴 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝑏))
12		pweq 4519	. . . . . 6 ⊢ (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
13	12	raleqdv 3318	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑)))
14		f1eq2 6600	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝐴–1-1→V))
15	14	rexbidv 3209	. . . . 5 ⊢ (𝑎 = 𝐴 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))
16	13, 15	imbi12d 348	. . . 4 ⊢ (𝑎 = 𝐴 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
17	11, 16	raleqbidv 3306	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
18	17	imbi2d 344	. 2 ⊢ (𝑎 = 𝐴 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))))
19		bi2.04 392	. . . . 5 ⊢ ((𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
20	19	albii 1827	. . . 4 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ ∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
21		19.21v 1947	. . . 4 ⊢ (∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
22	20, 21	bitri 278	. . 3 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
23		0elpw 5236	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑔
24		f10 6682	. . . . . . . . . . . . 13 ⊢ ∅:∅–1-1→V
25		f1eq1 6599	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑒:∅–1-1→V ↔ ∅:∅–1-1→V))
26	25	rspcev 3530	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ 𝒫 𝑔 ∧ ∅:∅–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V)
27	23, 24, 26	mp2an 692	. . . . . . . . . . . 12 ⊢ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V
28		f1eq2 6600	. . . . . . . . . . . . 13 ⊢ (𝑓 = ∅ → (𝑒:𝑓–1-1→V ↔ 𝑒:∅–1-1→V))
29	28	rexbidv 3209	. . . . . . . . . . . 12 ⊢ (𝑓 = ∅ → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V))
30	27, 29	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
32		n0 4251	. . . . . . . . . . 11 ⊢ (𝑓 ≠ ∅ ↔ ∃𝑖 𝑖 ∈ 𝑓)
33		snelpwi 5318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ∈ 𝒫 𝑓)
34		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → 𝑑 = {𝑖})
35		imaeq2 5914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → (𝑔 “ 𝑑) = (𝑔 “ {𝑖}))
36	34, 35	breq12d 5056	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = {𝑖} → (𝑑 ≼ (𝑔 “ 𝑑) ↔ {𝑖} ≼ (𝑔 “ {𝑖})))
37	36	rspcva 3528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → {𝑖} ≼ (𝑔 “ {𝑖}))
38		vex 3405	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑖 ∈ V
39	38	snnz 4682	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑖} ≠ ∅
40		snex 5313	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑖} ∈ V
41	40	0sdom 8766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∅ ≺ {𝑖} ↔ {𝑖} ≠ ∅)
42	39, 41	mpbir 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∅ ≺ {𝑖}
43		sdomdomtr 8768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ≺ {𝑖} ∧ {𝑖} ≼ (𝑔 “ {𝑖})) → ∅ ≺ (𝑔 “ {𝑖}))
44	42, 43	mpan 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → ∅ ≺ (𝑔 “ {𝑖}))
45		vex 3405	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
46	45	imaex 7683	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ {𝑖}) ∈ V
47	46	0sdom 8766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ≺ (𝑔 “ {𝑖}) ↔ (𝑔 “ {𝑖}) ≠ ∅)
48	44, 47	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → (𝑔 “ {𝑖}) ≠ ∅)
49	37, 48	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑔 “ {𝑖}) ≠ ∅)
50	49	expcom 417	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ({𝑖} ∈ 𝒫 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
51	33, 50	syl5 34	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
52	51	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
53	52	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
54	53	impr 458	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑔 “ {𝑖}) ≠ ∅)
55		n0 4251	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 “ {𝑖}) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
56	54, 55	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
57	45	imaex 7683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ∈ V
58	57	difexi 5210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ∖ {𝑗}) ∈ V
59	58	0dom 8765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})
60		breq1 5046	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = ∅ → (𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}) ↔ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
61	59, 60	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
63		simpll 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
64		elpwi 4512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
65	64	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
66		difsnpss 4710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 ∈ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓)
67	66	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 ∈ 𝑓 → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
68	67	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
69	65, 68	sspsstrd 4013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊊ 𝑓)
70		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≠ ∅)
71	69, 70	jca 515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅))
72		psseq1 3992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ⊊ 𝑓 ↔ 𝑐 ⊊ 𝑓))
73		neeq1 2997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ≠ ∅ ↔ 𝑐 ≠ ∅))
74	72, 73	anbi12d 634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ↔ (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅)))
75		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → ℎ = 𝑐)
76		imaeq2 5914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (𝑔 “ ℎ) = (𝑔 “ 𝑐))
77	75, 76	breq12d 5056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → (ℎ ≺ (𝑔 “ ℎ) ↔ 𝑐 ≺ (𝑔 “ 𝑐)))
78	74, 77	imbi12d 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ℎ = 𝑐 → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ↔ ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐))))
79	78	spvv 2005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) → ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐)))
80	63, 71, 79	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≺ (𝑔 “ 𝑐))
81		domdifsn 8717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ≺ (𝑔 “ 𝑐) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
83	82	expr 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 ≠ ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
84	62, 83	pm2.61dne 3021	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
85	84	adantlrr 721	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
86	85	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
87		df-ss 3874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ⊆ (𝑓 ∖ {𝑖}) ↔ (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
88	64, 87	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
89	88	imaeq2d 5918	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) = (𝑔 “ 𝑐))
90	89	ineq1d 4116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
91	90	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
92		indif2 4175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗})
93		imassrn 5929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ⊆ ran 𝑔
94		elpwi 4512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → 𝑔 ⊆ (𝑓 × 𝑏))
95		rnss 5797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ ran (𝑓 × 𝑏))
96		rnxpss 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ran (𝑓 × 𝑏) ⊆ 𝑏
97	95, 96	sstrdi 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
98	94, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
99	93, 98	sstrid 3902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 “ 𝑐) ⊆ 𝑏)
100		df-ss 3874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ⊆ 𝑏 ↔ ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
101	99, 100	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
102	101	difeq1d 4026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
103	102	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
104	92, 103	syl5eq 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
105	104	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
106	91, 105	eqtrd 2774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
107	86, 106	breqtrrd 5071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
108	107	ralrimiva 3098	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
109		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → 𝑐 = 𝑑)
110		imainrect 6033	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗}))
111		imaeq2 5914	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
112	110, 111	eqtr3id 2788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
113	109, 112	breq12d 5056	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
114	113	cbvralvw 3351	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
115	108, 114	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
116	115	adantllr 719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
117		inss2 4134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))
118		difss 4036	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∖ {𝑗}) ⊆ 𝑏
119		xpss2 5560	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ {𝑗}) ⊆ 𝑏 → ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
121	117, 120	sstri 3900	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
122	45	inex1 5199	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ V
123	122	elpw 4507	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
124	121, 123	mpbir 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)
125		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
126	67	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
127	126	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
128		vex 3405	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑓 ∈ V
129	128	difexi 5210	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∖ {𝑖}) ∈ V
130		psseq1 3992	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓))
131		xpeq1 5554	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 × 𝑏) = ((𝑓 ∖ {𝑖}) × 𝑏))
132	131	pweqd 4522	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏))
133		pweq 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ {𝑖}))
134	133	raleqdv 3318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑)))
135		f1eq2 6600	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ {𝑖})–1-1→V))
136	135	rexbidv 3209	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
137	134, 136	imbi12d 348	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
138	132, 137	raleqbidv 3306	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
139	130, 138	imbi12d 348	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))))
140	129, 139	spcv 3513	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
141	125, 127, 140	sylc 65	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
142		imaeq1 5913	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
143	142	breq2d 5055	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
144	143	ralbidv 3111	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
145		pweq 4519	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
146	145	rexeqdv 3319	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
147	144, 146	imbi12d 348	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
148	147	rspcva 3528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
149	124, 141, 148	sylancr 590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
150	116, 149	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)
151		f1eq1 6599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑘 → (𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ 𝑘:(𝑓 ∖ {𝑖})–1-1→V))
152	151	cbvrexvw 3352	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
153	150, 152	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
154		vex 3405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑗 ∈ V
155	38, 154	elimasn 5946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) ↔ ⟨𝑖, 𝑗⟩ ∈ 𝑔)
156	155	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → ⟨𝑖, 𝑗⟩ ∈ 𝑔)
157	156	snssd 4712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
158	157	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
159		elpwi 4512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
160		inss1 4133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ 𝑔
161	159, 160	sstrdi 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ 𝑔)
162	161	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → 𝑘 ⊆ 𝑔)
163	158, 162	unssd 4090	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
164	45	elpw2 5227	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
165	163, 164	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
166	165	ad2ant2lr 748	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
167	38, 154	f1osn 6689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗}
168	167	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗})
169		f1f1orn 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘:(𝑓 ∖ {𝑖})–1-1→V → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
170	169	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
171		disjdif 4376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅)
173		incom 4105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ({𝑗} ∩ ran 𝑘) = (ran 𝑘 ∩ {𝑗})
174	159, 117	sstrdi 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
175		rnss 5797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
176		rnxpss 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ (𝑏 ∖ {𝑗})
177	175, 176	sstrdi 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
178	174, 177	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
179		disjdifr 4377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅
180		ssdisj 4364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((ran 𝑘 ⊆ (𝑏 ∖ {𝑗}) ∧ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅) → (ran 𝑘 ∩ {𝑗}) = ∅)
181	178, 179, 180	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (ran 𝑘 ∩ {𝑗}) = ∅)
182	173, 181	syl5eq 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ({𝑗} ∩ ran 𝑘) = ∅)
183	182	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑗} ∩ ran 𝑘) = ∅)
184		f1oun 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((({⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗} ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘) ∧ (({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅ ∧ ({𝑗} ∩ ran 𝑘) = ∅)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
185	168, 170, 172, 183, 184	syl22anc 839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
186	185	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
187		snssi 4711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ⊆ 𝑓)
188	187	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → {𝑖} ⊆ 𝑓)
189		undif 4386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ⊆ 𝑓 ↔ ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
190	188, 189	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
191	190	f1oeq2d 6646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
192	191	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
193	186, 192	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘))
194		f1of1 6649	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘))
195		ssv 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑗} ∪ ran 𝑘) ⊆ V
196		f1ss 6610	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘) ∧ ({𝑗} ∪ ran 𝑘) ⊆ V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
197	194, 195, 196	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
198	193, 197	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
199		f1eq1 6599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑒 = ({⟨𝑖, 𝑗⟩} ∪ 𝑘) → (𝑒:𝑓–1-1→V ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V))
200	199	rspcev 3530	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ∧ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
201	166, 198, 200	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
202	201	rexlimdvaa 3197	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
203	202	ex 416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
204	203	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
205	204	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
206	205	impr 458	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
207	206	adantllr 719	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
208	153, 207	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
209	208	expr 460	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
210	209	expd 419	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
211	210	impr 458	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
212	211	exlimdv 1941	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
213	56, 212	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
214	213	expr 460	. . . . . . . . . . . 12 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
215	214	exlimdv 1941	. . . . . . . . . . 11 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
216	32, 215	syl5bi 245	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ≠ ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
217	31, 216	pm2.61dne 3021	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
218		exanali 1867	. . . . . . . . . 10 ⊢ (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) ↔ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
219		simprll 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊊ 𝑓)
220		pssss 4000	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ⊊ 𝑓 → ℎ ⊆ 𝑓)
221	219, 220	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊆ 𝑓)
222	221	sspwd 4518	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝒫 ℎ ⊆ 𝒫 𝑓)
223		simplrr 778	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
224		ssralv 3957	. . . . . . . . . . . . . . . . . 18 ⊢ (𝒫 ℎ ⊆ 𝒫 𝑓 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑)))
225	222, 223, 224	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑))
226		elpwi 4512	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ 𝒫 ℎ → 𝑑 ⊆ ℎ)
227		resima2 5875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
228	226, 227	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ 𝒫 ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
229	228	eqcomd 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑔 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
230	229	breq2d 5055	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
231	230	ralbiia 3080	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
232	225, 231	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
233		imaeq1 5913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑐 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
234	233	breq2d 5055	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
235	234	ralbidv 3111	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
236		pweq 4519	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → 𝒫 𝑐 = 𝒫 (𝑔 ↾ ℎ))
237	236	rexeqdv 3319	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
238	235, 237	imbi12d 348	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑔 ↾ ℎ) → ((∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)))
239		simpllr 776	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
240		psseq1 3992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (𝑎 ⊊ 𝑓 ↔ ℎ ⊊ 𝑓))
241		xpeq1 5554	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (𝑎 × 𝑏) = (ℎ × 𝑏))
242	241	pweqd 4522	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → 𝒫 (𝑎 × 𝑏) = 𝒫 (ℎ × 𝑏))
243		pweq 4519	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → 𝒫 𝑎 = 𝒫 ℎ)
244	243	raleqdv 3318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑)))
245		f1eq2 6600	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → (𝑒:𝑎–1-1→V ↔ 𝑒:ℎ–1-1→V))
246	245	rexbidv 3209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
247	244, 246	imbi12d 348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
248	242, 247	raleqbidv 3306	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
249	240, 248	imbi12d 348	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ℎ → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))))
250	249	spvv 2005	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
251	239, 219, 250	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
252		simplrl 777	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝑔 ∈ 𝒫 (𝑓 × 𝑏))
253		ssres 5867	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ ((𝑓 × 𝑏) ↾ ℎ))
254		df-res 5552	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ↾ ℎ) = ((𝑓 × 𝑏) ∩ (ℎ × V))
255		inxp 5690	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) = ((𝑓 ∩ ℎ) × (𝑏 ∩ V))
256		inss2 4134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∩ ℎ) ⊆ ℎ
257		inss1 4133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∩ V) ⊆ 𝑏
258		xpss12 5555	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑓 ∩ ℎ) ⊆ ℎ ∧ (𝑏 ∩ V) ⊆ 𝑏) → ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏))
259	256, 257, 258	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏)
260	255, 259	eqsstri 3925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) ⊆ (ℎ × 𝑏)
261	254, 260	eqsstri 3925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 × 𝑏) ↾ ℎ) ⊆ (ℎ × 𝑏)
262	253, 261	sstrdi 3903	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
263	94, 262	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
264	45	resex 5888	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ↾ ℎ) ∈ V
265	264	elpw 4507	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏) ↔ (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
266	263, 265	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
267	252, 266	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
268	238, 251, 267	rspcdva 3532	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
269	232, 268	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)
270		f1eq1 6599	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑖 → (𝑒:ℎ–1-1→V ↔ 𝑖:ℎ–1-1→V))
271	270	cbvrexvw 3352	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V ↔ ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
272	269, 271	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
273		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (ℎ ∪ 𝑐) → 𝑑 = (ℎ ∪ 𝑐))
274		imaeq2 5914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑔 “ 𝑑) = (𝑔 “ (ℎ ∪ 𝑐)))
275	273, 274	breq12d 5056	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑑 ≼ (𝑔 “ 𝑑) ↔ (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐))))
276		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
277	276	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
278	220	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ℎ ⊆ 𝑓)
279	278	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ⊆ 𝑓)
280		elpwi 4512	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ (𝑓 ∖ ℎ))
281		difss 4036	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ∖ ℎ) ⊆ 𝑓
282	280, 281	sstrdi 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ 𝑓)
283	282	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ⊆ 𝑓)
284	279, 283	unssd 4090	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ⊆ 𝑓)
285	128	elpw2 5227	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ ∪ 𝑐) ∈ 𝒫 𝑓 ↔ (ℎ ∪ 𝑐) ⊆ 𝑓)
286	284, 285	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ∈ 𝒫 𝑓)
287	275, 277, 286	rspcdva 3532	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐)))
288		imaundi 6002	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
289		undif2 4381	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
290	288, 289	eqtr4i 2765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
291	287, 290	breqtrdi 5084	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
292		simp-4l 783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑓 ∈ Fin)
293	292, 279	ssfid 8887	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ Fin)
294		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = ℎ → 𝑑 = ℎ)
295		imaeq2 5914	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = ℎ → (𝑔 “ 𝑑) = (𝑔 “ ℎ))
296	294, 295	breq12d 5056	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ ℎ ≼ (𝑔 “ ℎ)))
297		vex 3405	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℎ ∈ V
298	297	elpw 4507	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ ∈ 𝒫 𝑓 ↔ ℎ ⊆ 𝑓)
299	279, 298	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ 𝒫 𝑓)
300	296, 277, 299	rspcdva 3532	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≼ (𝑔 “ ℎ))
301		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ¬ ℎ ≺ (𝑔 “ ℎ))
302		bren2 8648	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ≈ (𝑔 “ ℎ) ↔ (ℎ ≼ (𝑔 “ ℎ) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)))
303	300, 301, 302	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≈ (𝑔 “ ℎ))
304	303	ensymd 8668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (𝑔 “ ℎ) ≈ ℎ)
305		incom 4105	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∩ 𝑐) = (𝑐 ∩ ℎ)
306		ssdifin0 4387	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (𝑐 ∩ ℎ) = ∅)
307	305, 306	syl5eq 2786	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
308	280, 307	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
309	308	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∩ 𝑐) = ∅)
310		disjdif 4376	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅
311	310	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)
312		domunfican 8933	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ ∈ Fin ∧ (𝑔 “ ℎ) ≈ ℎ) ∧ ((ℎ ∩ 𝑐) = ∅ ∧ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
313	293, 304, 309, 311, 312	syl22anc 839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
314	291, 313	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
315	101	difeq1d 4026	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
316	315	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
317	316	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
318	314, 317	breqtrrd 5071	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
319		df-ss 3874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) ↔ (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
320	280, 319	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
321	320	imaeq2d 5918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) = (𝑔 “ 𝑐))
322	321	ineq1d 4116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
323		indif2 4175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ))
324	322, 323	eqtrdi 2790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
325	324	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
326	318, 325	breqtrrd 5071	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
327	326	ralrimiva 3098	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
328		imainrect 6033	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ)))
329		imaeq2 5914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
330	328, 329	eqtr3id 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
331	109, 330	breq12d 5056	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
332	331	cbvralvw 3351	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
333	327, 332	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
334	333	adantllr 719	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
335		inss2 4134	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))
336		difss 4036	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏
337		xpss2 5560	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏 → ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
338	336, 337	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
339	335, 338	sstri 3900	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
340	45	inex1 5199	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ V
341	340	elpw 4507	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
342	339, 341	mpbir 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)
343		incom 4105	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∩ ℎ) = (ℎ ∩ 𝑓)
344		df-ss 3874	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∩ 𝑓) = ℎ)
345	220, 344	sylib 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ⊊ 𝑓 → (ℎ ∩ 𝑓) = ℎ)
346	343, 345	syl5eq 2786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ ⊊ 𝑓 → (𝑓 ∩ ℎ) = ℎ)
347	346	neeq1d 2994	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ⊊ 𝑓 → ((𝑓 ∩ ℎ) ≠ ∅ ↔ ℎ ≠ ∅))
348	347	biimpar 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∩ ℎ) ≠ ∅)
349		disj4 4363	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∩ ℎ) = ∅ ↔ ¬ (𝑓 ∖ ℎ) ⊊ 𝑓)
350	349	bicomi 227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑓 ∖ ℎ) ⊊ 𝑓 ↔ (𝑓 ∩ ℎ) = ∅)
351	350	necon1abii 2983	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∩ ℎ) ≠ ∅ ↔ (𝑓 ∖ ℎ) ⊊ 𝑓)
352	348, 351	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∖ ℎ) ⊊ 𝑓)
353	352	ad2antrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ∖ ℎ) ⊊ 𝑓)
354	128	difexi 5210	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∖ ℎ) ∈ V
355		psseq1 3992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ ℎ) ⊊ 𝑓))
356		xpeq1 5554	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 × 𝑏) = ((𝑓 ∖ ℎ) × 𝑏))
357	356	pweqd 4522	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ ℎ) × 𝑏))
358		pweq 4519	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ ℎ))
359	358	raleqdv 3318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑)))
360		f1eq2 6600	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ ℎ)–1-1→V))
361	360	rexbidv 3209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
362	359, 361	imbi12d 348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
363	357, 362	raleqbidv 3306	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
364	355, 363	imbi12d 348	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))))
365	354, 364	spcv 3513	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
366	239, 353, 365	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
367		imaeq1 5913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
368	367	breq2d 5055	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
369	368	ralbidv 3111	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
370		pweq 4519	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
371	370	rexeqdv 3319	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
372	369, 371	imbi12d 348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)))
373	372	rspcva 3528	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
374	342, 366, 373	sylancr 590	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
375	334, 374	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)
376		f1eq1 6599	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑗 → (𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ 𝑗:(𝑓 ∖ ℎ)–1-1→V))
377	376	cbvrexvw 3352	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
378	375, 377	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
379		elpwi 4512	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ (𝑔 ↾ ℎ))
380		resss 5865	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ↾ ℎ) ⊆ 𝑔
381	379, 380	sstrdi 3903	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ 𝑔)
382	381	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖 ⊆ 𝑔)
383	382	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖 ⊆ 𝑔)
384		elpwi 4512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
385		inss1 4133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ 𝑔
386	384, 385	sstrdi 3903	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ 𝑔)
387	386	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗 ⊆ 𝑔)
388	383, 387	unssd 4090	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ⊆ 𝑔)
389	45	elpw2 5227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ↔ (𝑖 ∪ 𝑗) ⊆ 𝑔)
390	388, 389	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ∈ 𝒫 𝑔)
391		f1f1orn 6661	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖:ℎ–1-1→V → 𝑖:ℎ–1-1-onto→ran 𝑖)
392	391	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖:ℎ–1-1-onto→ran 𝑖)
393	392	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖:ℎ–1-1-onto→ran 𝑖)
394		f1f1orn 6661	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗:(𝑓 ∖ ℎ)–1-1→V → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
395	394	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
396		disjdif 4376	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∩ (𝑓 ∖ ℎ)) = ∅
397	396	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∩ (𝑓 ∖ ℎ)) = ∅)
398		rnss 5797	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ⊆ (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
399	379, 398	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
400		df-ima 5553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔 “ ℎ) = ran (𝑔 ↾ ℎ)
401	399, 400	sseqtrrdi 3942	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ (𝑔 “ ℎ))
402	401	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → ran 𝑖 ⊆ (𝑔 “ ℎ))
403	402	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑖 ⊆ (𝑔 “ ℎ))
404		incom 4105	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ran 𝑗) = (ran 𝑗 ∩ (𝑔 “ ℎ))
405	384, 335	sstrdi 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
406		rnss 5797	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
407	405, 406	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
408		rnxpss 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ (𝑏 ∖ (𝑔 “ ℎ))
409	407, 408	sstrdi 3903	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
410	409	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
411		disjdifr 4377	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅
412		ssdisj 4364	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)) ∧ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
413	410, 411, 412	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
414	404, 413	syl5eq 2786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅)
415		ssdisj 4364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑖 ⊆ (𝑔 “ ℎ) ∧ ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅) → (ran 𝑖 ∩ ran 𝑗) = ∅)
416	403, 414, 415	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑖 ∩ ran 𝑗) = ∅)
417		f1oun 6669	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖:ℎ–1-1-onto→ran 𝑖 ∧ 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗) ∧ ((ℎ ∩ (𝑓 ∖ ℎ)) = ∅ ∧ (ran 𝑖 ∩ ran 𝑗) = ∅)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
418	393, 395, 397, 416, 417	syl22anc 839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
419		undif 4386	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
420	419	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
421	420	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
422	421	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
423	422	f1oeq2d 6646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
424	418, 423	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
425		f1of1 6649	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
426	424, 425	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
427		ssv 3915	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝑖 ∪ ran 𝑗) ⊆ V
428		f1ss 6610	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗) ∧ (ran 𝑖 ∪ ran 𝑗) ⊆ V) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
429	426, 427, 428	sylancl 589	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
430		f1eq1 6599	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖 ∪ 𝑗) → (𝑒:𝑓–1-1→V ↔ (𝑖 ∪ 𝑗):𝑓–1-1→V))
431	430	rspcev 3530	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ∧ (𝑖 ∪ 𝑗):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
432	390, 429, 431	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
433	432	rexlimdvaa 3197	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
434	433	rexlimdvaa 3197	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
435	252, 221, 434	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
436	272, 378, 435	mp2d 49	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
437	436	ex 416	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
438	437	exlimdv 1941	. . . . . . . . . . 11 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
439	438	imp 410	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
440	218, 439	sylan2br 598	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
441	217, 440	pm2.61dan 813	. . . . . . . 8 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
442	441	exp32 424	. . . . . . 7 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
443	442	ralrimiv 3097	. . . . . 6 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
444		imaeq1 5913	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 “ 𝑑) = (𝑐 “ 𝑑))
445	444	breq2d 5055	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ (𝑐 “ 𝑑)))
446	445	ralbidv 3111	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
447		pweq 4519	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → 𝒫 𝑔 = 𝒫 𝑐)
448	447	rexeqdv 3319	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
449	446, 448	imbi12d 348	. . . . . . 7 ⊢ (𝑔 = 𝑐 → ((∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
450	449	cbvralvw 3351	. . . . . 6 ⊢ (∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
451	443, 450	sylib 221	. . . . 5 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
452	451	exp31 423	. . . 4 ⊢ (𝑓 ∈ Fin → (𝑏 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
453	452	a2d 29	. . 3 ⊢ (𝑓 ∈ Fin → ((𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
454	22, 453	syl5bi 245	. 2 ⊢ (𝑓 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
455	9, 18, 454	findcard3 8903	1 ⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541   = wceq 1543  ∃wex 1787   ∈ wcel 2110   ≠ wne 2935  ∀wral 3054  ∃wrex 3055  Vcvv 3401   ∖ cdif 3854   ∪ cun 3855   ∩ cin 3856   ⊆ wss 3857   ⊊ wpss 3858  ∅c0 4227  𝒫 cpw 4503  {csn 4531  ⟨cop 4537   class class class wbr 5043   × cxp 5538  ran crn 5541   ↾ cres 5542   “ cima 5543  –1-1→wf1 6366  –1-1-onto→wf1o 6368   ≈ cen 8612   ≼ cdom 8613   ≺ csdm 8614  Fincfn 8615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3403  df-sbc 3688  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-pss 3876  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-tp 4536  df-op 4538  df-uni 4810  df-br 5044  df-opab 5106  df-tr 5151  df-id 5444  df-eprel 5449  df-po 5457  df-so 5458  df-fr 5498  df-we 5500  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-ord 6205  df-on 6206  df-lim 6207  df-suc 6208  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-om 7634  df-1o 8191  df-er 8380  df-en 8616  df-dom 8617  df-sdom 8618  df-fin 8619

This theorem is referenced by:  marypha1  9039